Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-09T19:02:46.371Z Has data issue: false hasContentIssue false
  • English
  • Français

Proof nets and semi-star-autonomous categories

Published online by Cambridge University Press:  10 November 2014

WILLEM HEIJLTJES  and
LUTZ STRAßBURGER
WILLEM HEIJLTJES
Affiliation:
Department of Computer Science, University of Bath, Claverton Down, Bath BA2 7AY, UK Email: w.b.heijltjes@bath.ac.uk
LUTZ STRAßBURGER
Affiliation:
INRIA Saclay, 1 rue Honoré d'Estienne d'Orves, École Polytechnique, 91120 PalaiseauFrance Email: lutz@lix.polytechnique.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

In this paper, it is proved that Girard's proof nets for multiplicative linear logic characterize free semi-star-autonomous categories.

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Issue 5 , June 2016 , pp. 789 - 828
Copyright
Copyright © Cambridge University Press 2014 

References

Barr, M. (1991) *-Autonomous categories and linear logic. Mathematical Structures in Computer Science 1 159–178.CrossRefGoogle Scholar
Blute, R. (1993) Linear logic, coherence, and dinaturality. Theoretical Computer Science 115 3–41.Google Scholar
Blute, R., Cockett, R., Seely, R. and Trimble, T. (1996) Natural deduction and coherence for weakly distributive categories. Journal of Pure and Applied Algebra 113 229–296.Google Scholar
Cockett, R. and Seely, R. (1997) Weakly distributive categories. Journal of Pure and Applied Algebra 114 (2)133–173.Google Scholar
Danos, V. and Regnier, L. (1989) The structure of multiplicatives. Archive for Mathematical Logic 28 181–203.Google Scholar
Day, B. (1970) On closed categories of functors. In: Reports of the Midwest Category Seminar IV. Springer Lecture Notes in Mathematics 137 1–38.CrossRefGoogle Scholar
Došen, K. and Petrić, Z. (2005) Proof-Net Categories, Polimetrica, Milan.Google Scholar
Girard, J.-Y. (1987) Linear logic. Theoretical Computer Science 50 (1)1–102.Google Scholar
Heijltjes, W. (2011) Proof nets for additive linear logic with units. In: Proceedings Logic in Computer Science 207–216.Google Scholar
Heijltjes, W. and Houston, R. (2014) No proof nets for MLL: Proof equivalence in MLL with units is PSPACE-complete. In: Proceedings of the Joint Meeting of Computer Science Logic and Logic in Computer Science (CSL-LICS) 2014. Proceedings Logic in Computer Science. To appear.Google Scholar
Houston, R. (2008) Modelling Linear Logic without Units, Ph.D. thesis, University of Manchester.Google Scholar
Hughes, D. J. (2012) Simple free star-autonomous categories and full coherence. Journal of Pure and Applied Algebra 216 (11)2386–2410.Google Scholar
Joyal, A. and Street, R. (1991) The geometry of tensor calculus, I. Advances in Mathematics 88 55–112.Google Scholar
Kelly, G. M. (1964) On MacLane's conditions for coherence of natural associators, commutativites, etc. Journal of Algebra 1 397–402.Google Scholar
Kelly, G. M. (1982) Basic Concepts of Enriched Category Theory, London Mathematical Society Lecture Notes Series, volume 64, Cambridge University Press.Google Scholar
Kelly, G. M. and Mac Lane, S. (1971) Coherence in closed categories. Journal of Pure and Applied Algebra 1 97–140.Google Scholar
Lafont, Y. (1995) From proof nets to interaction nets. In: Advances in Linear Logic, London Mathematical Society Lecture Notes, volume 222, Cambridge University Press 225–247.CrossRefGoogle Scholar
Lamarche, F. and Straßburger, L. (2005) Constructing free Boolean categories. Proceedings Logic in Computer Science, 209–218.Google Scholar
Lamarche, F. and Straßburger, L. (2006) From proof nets to the free *-autonomous category. Logical Methods in Computer Science 2 (4:3) 1–44.Google Scholar
Mac Lane, S. (1963) Natural associativity and commutativity. Rice University Studies 49 28–46.Google Scholar
Selinger, P. (2011) A survey of graphical languages for monoidal categories. Lecture Notes in Physics 813 289–355.Google Scholar