INTRODUCTION TO LUDICS

Ludics departs from the syntax/semantics dichotomy by putting forward an internal (monist) approach to the explanation of logic / programming. It builds on some ideas from linear logic (resource consciousness, geometry of proofs, and more recently, polarization), and on the computation-as-interaction paradigm underlying previous works on sequentiality and games semantics.

Two saliant new features in ludics are:

• Locativity: one realises that usual logic (including linear logic) is "spiritual", i.e., up to isomorphism: typically, the usual (additive) conjunction enjoys commutativity and associativity only up to isomorphism. But there is a deeper locative level, with indeed a more regular structure. In ludics, conjunction can be defined in terms of a plain intersection and of explicit delocalisations. Intersection is really associative, commutative, etc. (no isomorphisms), and corresponds to intersection types, subtyping, etc...
• Daimon: How can a proof of A interact with a "proof" of (not A)? By allowing incomplete proofs. This closely corresponds to the use of errors for observing program behaviour.