We present a game-based semantic framework in which the time complexity of any MELL 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 abstraction result.
U. Dal Lago, O. Laurent (2008). Quantitative Game Semantics for Linear Logic. BERLIN : SPRINGER.
Quantitative Game Semantics for Linear Logic
DAL LAGO, UGO;
2008
Abstract
We present a game-based semantic framework in which the time complexity of any MELL 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 abstraction result.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
