Abstract
Indexed categories provide models of cartesian calculi of explicit substitutions. However, these structures are inherently non-linear and hence cannot be used to model linear calculi of explicit substitution. This paper replaces indexed categories with pre-sheaves, thus providing a categorical semantics covering both the linear and cartesian cases. We further justify our models by proving soundness and completeness results.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jaques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.
F. J Alberti. An abstract machine based on linear logic and explicit substitutions. Master’s thesis, School of Computer Science, University of Birmingham, 1997.
A. Barber and G. Plotkin. Dual intuitionistic linear logic. Technical report, LFCS, University of Edinburgh, 1997.
N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 75–90. Springer Verlag, 1993.
Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Proceedings of Computer Science Logic’ 94, Kazimierz, Poland. Lecture Notes in Computer Science No. 933, Berlin, Heidelberg, New York, 1995.
Gavin Bierman. On Intuitionistic Linear Logic. Phd-thesis, University of Cambridge, 1994. Also available as Technical Report No. 346.
Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The categorical abstract machine. Science of Computer Programming, 8:173–202, 1987.
Thomas Ehrhard. A categorical semantics of constructions. In Third Annual Symposium on Logic in Computer Science, pages 264–273. IEEE, 1988.
N. Ghani. Adjoint Rewriting. PhD thesis, University of Edinburgh, 1995.
N. Ghani, V. de Paiva, and E. Ritter. Linear explicit substitutions. In Proc. of Westapp’98, 1998. Full version submitted for publication.
J. M. E. Hyland and A. M. Pitts. The theory of constructions: Categorical semantics and topos theoretic models. Contemporary Mathematics, 92:137–198, 1989.
Bart Jacobs. Simply typed and untyped lambda calculus revisited. In Michael Fourman, Peter Johnstone, and Andrew Pitts, editors, Applications of Categories in Computer Science, LMS Lecture Note Series 177, pages 119–142. CUP, 1992.
Yves Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.
Ian Mackie. Lilac: A functional programming language based on linear logic. Journal of Functional Programming, 4(4):395–433, 1994.
E. Ritter and V. de Paiva. On explicit substitution and names (extended abstract). In Proc. of ICALP’97, LNCS 1256, pages 248–258, 1997.
Eike Ritter. Categorical abstract machines for higher-order lambda calculi. Theoretical Computer Science, 136(1):125–162, 1994.
R. A. G. Seely. Linear logic, *-autonomous categories and cofree algebras. Contemporary Mathematics, 92, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghani, N., de Paiva, V., Ritter, E. (1999). Categorical Models of Explicit Substitutions. In: Thomas, W. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 1999. Lecture Notes in Computer Science, vol 1578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49019-1_14
Download citation
DOI: https://doi.org/10.1007/3-540-49019-1_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65719-4
Online ISBN: 978-3-540-49019-7
eBook Packages: Springer Book Archive