Ludics with Repetitions (Exponentials, Interactive Types and Completeness)

Abstract. Ludics is peculiar in the panorama of game semantics: we first have the definition of interaction-composition and then we have semantical types, as a set of strategies which “behave well” and react in the same way to a set of tests. The semantical types which are interpretation of logical formulas enjoy a fundamental property, called internal completeness, which characterizes ludics and sets it apart also from realizability. Internal completeness entails standard full completeness as a consequence. A growing body of works start to explore the potentiality of this specific interactive approach. However, ludics has two main limitations, which are consequence of the fact the original formulation, strategies are abstractions of MALL proofs. On one side, no repetitions are allowed. On the other side, there is a huge amount of structure, and the proofs tend to rely on the very specific properties of the MALL proof-like strategies, making it difficult to transfer the approac...

• Type: Conference
• Year: 2009
• Where: LICS
• Authors: Michele Basaldella, Claudia Faggian
• Keywords: Computer Science, Internal Completeness, LICS 2009, Ludics, Semantical Types