Towards a Typed Geometry of Interaction

  • Esfandiar Haghverdi
  • Philip J. Scott
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


Girard’s Geometry of Interaction (GoI) develops a mathematical framework for modelling the dynamics of cut-elimination. We introduce a typed version of GoI, called Multiobject GoI (MGoI) for multiplicative linear logic without units in categories which include previous (untyped) GoI models, as well as models not possible in the original untyped version. The development of MGoI depends on a new theory of partial traces and trace classes, as well as an abstract notion of orthogonality (related to work of Hyland and Schalk) We develop Girard’s original theory of types, data and algorithms in our setting, and show his execution formula to be an invariant of Cut Elimination. We prove Soundness and Completeness Theorems for the MGoI interpretation in partially traced categories with an orthogonality.


Monoidal Category Linear Logic Trace Class Dimensional Vector Space Orthogonality Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)Google Scholar
  2. 2.
    Abramsky, S., Blute, R., Panangaden, P.: Nuclear and trace ideals in tensored *-categories. J. Pure and Applied Algebra 143, 3–47 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Abramsky, S., Haghverdi, E., Scott, P.J.: Geometry of Interaction and Linear Combinatory Algebras. MSCS 12(5), 625–665 (2002)zbMATHMathSciNetGoogle Scholar
  4. 4.
    Abramsky, S., Jagadeesan, R.: New Foundations for the Geometry of Interaction. Information and Computation 111(1), 53–119 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Baillot, P.: Abramsky-Jagadeesan-Malacaria strategies and the geometry of interaction, mémoire de DEA, Universite Paris 7 (1995)Google Scholar
  6. 6.
    Baillot, P., Pedicini, M.: Elementary complexity and geometry of interaction. Fundamenta Informaticae 45(1-2) (2001)Google Scholar
  7. 7.
    Danos, V.: La logique linéaire appliquée à l’étude de divers processus de normalisation et principalement du λ-calcul. PhD thesis, Université Paris VII (1990)Google Scholar
  8. 8.
    Danos, V., Regnier, L.: Proof-nets and the Hilbert Space. In: Advances in Linear Logic. London Math. Soc. Notes, vol. 222, CUP, pp. 307–328 (1995)Google Scholar
  9. 9.
    Gonthier, G., Abadi, M., Lévy, J.-J.: The geometry of optimal lambda reduction. In: Proceedings of Logic in Computer Science, vol. 9 pp. 15–26 (1992)Google Scholar
  10. 10.
    Girard, J.-Y.: Linear Logic. Theoretical Computer Science 50(1), 1–102 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Girard, J.-Y.: Geometry of Interaction I: Interpretation of System F. In: Proc. Logic Colloquium 1988, pp. 221–260. North Holland, Amsterdam (1989a)Google Scholar
  13. 13.
    Girard, J.-Y.: Geometry of Interaction III: Accommodating the Additives. In: Advances in Linear Logic. LNS, vol. 222, CUP, pp. 329–389 (1995)Google Scholar
  14. 14.
    Girard, J.-Y.: Cours de Logique, Rome (2004) (forthcoming)Google Scholar
  15. 15.
    Haghverdi, E.: A Categorical Approach to Linear Logic, Geometry of Proofs and Full Completeness, PhD Thesis, University of Ottawa, Canada (2000)Google Scholar
  16. 16.
    Haghverdi, E.: Unique Decomposition Categories, Geometry of Interaction and combinatory logic. Math. Struct. in Comp. Science 10, 205–231 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Haghverdi, E., Scott, P.J.: A categorical model for the Geometry of Interaction. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 708–720. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Haghverdi, E., Scott, P.J.: From Geometry of Interaction to Denotational Semantics. In: Proceedings of CTCS 2004. ENTCS, vol. 122, pp. 67–87. Elsevier, Amsterdam (2004)Google Scholar
  19. 19.
    Hasegawa, M.: Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculus. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 196–213. Springer, Heidelberg (1997)Google Scholar
  20. 20.
    Hines, P.: A categorical framework for finite state machines. Math. Struct. in Comp. Science 13, 451–480 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Hyland, M., Schalk, A.: Glueing and Orthogonality for Models of Linear Logic. Theoretical Computer Science 294, 183–231 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Jeffrey, A.S.A.: Premonoidal categories and a graphical view of programs (1998), See the webpage Also: Electr. Notes Theor. Comput. Sci. 10 (1997)
  23. 23.
    Joyal, A., Street, R., Verity, D.: Traced Monoidal Categories. Math. Proc. Camb. Phil. Soc. 119, 447–468 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Laurent, O.: A Token Machine for Full Geometry of Interaction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 283–297. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  25. 25.
    Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  26. 26.
    Malacaria, P., Regnier, L.: Some Results on the Interpretation of λ- calculus in Operator Algebras. In: Proc. LICS, pp. 63–72. IEEE Press, Los Alamitos (1991)Google Scholar
  27. 27.
    Plotkin, G.: Trace Ideals, MFPS, invited lecture, Montreal (2003)Google Scholar
  28. 28.
    Regnier, L.: Lambda-calcul et Réseaux, PhD Thesis, Université Paris VII (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Esfandiar Haghverdi
    • 1
  • Philip J. Scott
    • 2
  1. 1.School of InformaticsIndiana UniversityBloomingtonUSA
  2. 2.Dept. of Mathematics & StatisticsUniversity of OttawaOttawaCanada

Personalised recommendations