In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic.
Key features of ludics include notion of compound connectives, using a technique known as focusing or focalisation (invented by the computer scientist Jean-Marc Andreoli), and its use of locations or loci over a base instead of propositions.
More precisely, ludics tries to retrieve known logical connectives and proof behaviours by following the paradigm of interactive computation, similarly to what is done in game semantics to which it is closely related.
The primary achievement of ludics is the discovery of a relationship between two natural, but distinct notions of type, or proposition.
Girard shows that for second-order affine linear logic, given a computational system with nontermination and error stops as effects, realizability and focalization give the same meaning to types.