Abstract
In a recent paper we introduced a typed version of Geometry of Interaction, called the Multi-object Geometry of Interaction (MGoI). Using this framework we gave an interpretation for the unit-free multiplicative fragment of linear logic. In this paper, we extend our work to cover the exponentials. We introduce the notion of a GoI Category that embodies the necessary ingredients for an MGoI interpretation for unit-free multiplicative and exponential linear logic.
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.: Retracing Some Paths in Process Algebra. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 1–17. Springer, Heidelberg (1996)
Abramsky, S., Blute, R., Panangaden, P.: Nuclear and trace ideals in tensored categories. J. Pure and Applied Algebra 143, 3–47 (1999)
Abramsky, S., Haghverdi, E., Scott, P.J.: Geometry of Interaction and Linear Combinatory Algebras. MSCS 12(5), 625–665 (2002)
Abramsky, S., Jagadeesan, R.: New Foundations for the Geometry of Interaction. Information and Computation 111(1), 53–119 (1994)
Girard, J.-Y.: Linear Logic. Theoretical Computer Science 50(1), 1–102 (1987)
Girard, J.-Y.: Geometry of Interaction II: Deadlock-free Algorithms. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 76–93. Springer, Heidelberg (1990)
Girard, J.-Y.: Geometry of Interaction I: Interpretation of System F. In: Proc. Logic Colloquium 88, pp. 221–260. North Holland, Amsterdam (1989)
Girard, J.-Y.: Geometry of Interaction III: Accommodating the Additives. In: Advances in Linear Logic, LNS 222,CUP, 329–389 (1995)
Girard, J.-Y. Cours de Logique, Rome 2004, Forthcoming (2004), Also available at http://iml.univ-mrs.fr/~girard/coursang/coursang.html
Haghverdi, E.: A Categorical Approach to Linear Logic, Geometry of Proofs and Full Completeness, PhD Thesis, University of Ottawa, Canada (2000)
Haghverdi, E., Scott, P.J.: A Categorical Model for the Geometry of Interaction. Theoretical Computer Science 350, 252–274 (2006)
Haghverdi, E., Scott, P.J.: Towards a Typed Geometry of Interaction, CSL2005 (Computer Science Logic), Luke Ong, SLNCS 3634. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 216–231. Springer, Heidelberg (2005)
Hyland, M., Schalk, A.: Glueing and Orthogonality for Models of Linear Logic. Theoretical Computer Science 294, 183–231 (2003)
Joyal, A., Street, R., Verity, D.: Traced Monoidal Categories. Math. Proc. Camb. Phil. Soc. 119, 447–468 (1996)
Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haghverdi, E. (2006). Typed GoI for Exponentials. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds) Automata, Languages and Programming. ICALP 2006. Lecture Notes in Computer Science, vol 4052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11787006_33
Download citation
DOI: https://doi.org/10.1007/11787006_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35907-4
Online ISBN: 978-3-540-35908-1
eBook Packages: Computer ScienceComputer Science (R0)