Abstract
This paper re-addresses the old problem of providing a categorical model for Intuitionistic Linear Logic (ILL). In particular we compare the now standard model proposed by Seely to the lesser known one proposed by Benton, Bierman, Hyland and de Paiva. Surprisingly we find that Seely's model is unsound in that it does not preserve equality of proofs. We shall propose how to adapt Seely's definition so as to correct this problem and consider how this compares with the model due to Benton et al.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1–2):3–57, 1993. Previously Available as Department of Computing, Imperial College Technical Report 90/20, 1990.
M. Barr. ⋆-autonomous categories and linear logic. Mathematical Structures in Computer Science, 1:159–178, 1991.
P.N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. Technical Report 352, Computer Laboratory, University of Cambridge, 1994.
P.N. Benton, G.M. Bierman, V.C.V. de Paiva, and J.M.E. Hyland. Term assignment for intuitionistic linear logic. Technical Report 262, Computer Laboratory, University of Cambridge, August 1992.
P.N. Benton, G.M. Bierman, V.C.V. de Paiva, and J.M.E. Hyland. A term calculus for intuitionistic linear logic. In M. Bezem and J.F. Groote, editors, Proceedings of Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 75–90, 1993.
G.M. Bierman. On Intuitionistic Linear Logic. PhD thesis, Computer Laboratory, University of Cambridge, December 1993. Available as Computer Laboratory Technical Report 346. August 1994.
J. Gallier. Constructive logics part I: A tutorial on proof systems and typed λ-calculi. Theoretical Computer Science, 110(2):249–339, March 1993.
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–101, 1987.
J.-Y. Girard and Y. Lafont. Linear logic and lazy computation. In Proceedings of TAPSOFT 87, volume 250 of Lecture Notes in Computer Science, pages 52–66, 1987. Previously Available as INRIA Report 588, 1986.
W.A. Howard. The formulae-as-types notion of construction. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980.
Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988. Corrections ibid. 62:327–328, 1988.
J. Lambek and P.J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1987.
S. Mac Lane. Categories for the Working Mathematican, volume 5 of Graduate Texts in Mathematics. Springer Verlag, 1971.
R.A.G. Seely. Linear logic, ⋇-autonomous categories and cofree algebras. In Conference on Categories in Computer Science and Logic, volume 92 of AMS Contemporary Mathematics, pages 371–382, June 1989.
A.S. Troelstra. Lectures on Linear Logic, volume 29 of Lecture Notes. CSLI, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bierman, G.M. (1995). What is a categorical model of Intuitionistic Linear Logic?. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014046
Download citation
DOI: https://doi.org/10.1007/BFb0014046
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59048-4
Online ISBN: 978-3-540-49178-1
eBook Packages: Springer Book Archive