Abstract
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 abstraction result.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S.: Semantics of interaction. In: Dybjer, P., Pitts, A. (eds.) Semantics and Logics of Computation. Publications of the Newton Institute, pp. 1–32. Cambridge University Press, Cambridge (1997)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163(2), 409–470 (2000)
Baillot, P.: Approches dynamiques en sémantique de la logique linéaire : jeux et géométrie de l’interaction. Thèse de doctorat, Université Aix-Marseille II (1999)
Baillot, P., Pedicini, M.: Elementary complexity and geometry of interaction. Fundamenta Informaticae 45(1-2), 1–31 (2001)
Lago, U.D.: Context semantics, linear logic and computational complexity. In: Proc. 21st Symposium on Logic in Computer Science, pp. 169–178. IEEE, Los Alamitos (2006)
Danos, V., Herbelin, H., Regnier, L.: Games semantics and abstract machines. In: Proc. 11th Symposium on Logic In Computer Science, pp. 394–405. IEEE, Los Alamitos (1996)
de Carvalho, D., Pagani, M., de Falco, L.T.: A semantic measure of the execution time in linear logic. Technical Report 6441, INRIA (2007)
Ghica, D.: Slot games: A quantitative model of computation. In: Proc. 32nd ACM Symposium on Principles of Programming Languages, pp. 85–97 (2005)
Girard, J.-Y.: Geometry of interaction III: accommodating the additives. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol. 222, pp. 329–389. Cambridge University Press, Cambridge (1995)
Hyland, M.: Game semantics. In: Dybjer, P., Pitts, A. (eds.) Semantics and Logics of Computation. Publications of the Newton Institute, pp. 131–184. Cambridge University Press, Cambridge (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dal Lago, U., Laurent, O. (2008). Quantitative Game Semantics for Linear Logic. In: Kaminski, M., Martini, S. (eds) Computer Science Logic. CSL 2008. Lecture Notes in Computer Science, vol 5213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-87531-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87530-7
Online ISBN: 978-3-540-87531-4
eBook Packages: Computer ScienceComputer Science (R0)