Proofs in Ludics are represented by designs. Designs (des-seins) can be seen as an intermediate syntax between sequent calculus and proof nets, carrying advantages from both approaches, especially w.r.t. cut-elimination. To study interaction between designs and develop a geometrical intuition, we introduce an abstract machine which presents normalization as a token travelling along a net of designs. This allows a concrete approach, from which to carry on the study of issues such as: (ⅰ) which part of a design can be recognized interactively; (ⅱ) how to reconstruct a design from the traces of its interactions in different tests.
展开▼
