Quantitative Game Semantics for Linear Logic

We present a game-based semantic framework in which the time complexity of any IMELL proof can be read out of its interpretation. This gives a compositional view of the geometry of interaction framework introduced by the first author. In our model the time measure is given by means of slots, as introduced by Ghica in a recent paper. The cost associated to a strategy is polynomially related to the normalization time of the interpreted proof, in the style of a complexity-theoretical full ion result.

• Type: Conference
• Year: 2008
• Where: CSL
• Authors: Ugo Dal Lago, Olivier Laurent
• Keywords: Automated Reasoning, CSL 2008, Game-based Semantic Framework, IMELL Proof, Time Complexity