Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-08T09:23:08.161Z Has data issue: false hasContentIssue false
  • English
  • Français

Classical lambda calculus in modern dress

Published online by Cambridge University Press:  13 July 2015

J.M.E. HYLAND
J.M.E. HYLAND*
Affiliation:
Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, Cambridge, UK Email: m.hyland@dpmms.cam.ac.uk
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.

Recent developments in the categorical foundations of universal algebra have given an impetus to an understanding of the lambda calculus coming from categorical logic: an interpretation is a semi-closed algebraic theory. Scott's representation theorem is then completely natural and leads to a precise Fundamental Theorem showing the essential equivalence between the categorical and more familiar notions.

References

Aczel, P. (1980). Frege structures and the notions of proposition, truth and set. In: Barwise, J., Keisler, H. J. and Kunen, K. (eds.) The Kleene Symposium, North-Holland 31–59.CrossRefGoogle Scholar
Adámek, J., Rosický, J. and Vitale, E. M. (2011). Algebraic Theories. Cambridge Tracts in Mathematics vol. 184, Cambridge University Press.Google Scholar
Barendregt, H. P. (1981) The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics vol. 103, North-Holland.Google Scholar
Barendregt, H. P. (1984). The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics vol. 103, North-Holland.Google Scholar
Barendregt, H. and Koymans, C. P. J. (1980). Comparing some classes of lambda calculus models. In: Seldin, J. P. and Hindley, J. R. (eds.) To H. B. Curry: Essays on Combinatory Logic and Formalism, Academic Press 287–301.Google Scholar
Barendregt, H. and Longo, G. (1980). Equality of lambda terms in the model Tω. In: Seldin, J. P. and Hindley, J. R. (eds.) To H. B. Curry: Essays on Combinatory Logic and Formalism, Academic Press 303–337.Google Scholar
Benton, N., Bierman, G., de Paiva, V. and Hyland, M. (1993). A term calculus for intuitionistic linear logic. In: Bezem, M. and Groote, J. F. (eds.) Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA 93. Springer-Verlag Lecture Notes in Computer Science 664 179–194.Google Scholar
Böhm, C. (1968). Alcune proprietà delle forme β-η-normali nel λ - K-calcolo. Pubblicazioni dell' Istituto per le Applicazioni del Calcolo 696 19 Roma.Google Scholar
Carraro, A. (2011). Models and Theories of Pure and Resource Lambda Calculi, Ph.D. thesis, Paris VII and Venezia.Google Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 1–41.Google Scholar
Ehrhard, T. and Regnier, L. (2006). Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms. Lecture Notes in Computer Science 3988 186–197.Google Scholar
Fiore, M., Gambino, N., Hyland, M. and Winskel, G. (1999). Kleisli bicategories. In: preparation.Google Scholar
Fiore, M., Plotkin, G. and Turi, D. (1999). Abstract syntax and variable binding. In: Proceedings 14th Annual IEEE Symposium on Logic in Computer Science 193–202.Google Scholar
Freyd, P. J. (1989). Combinators. In: Gray, J. W. and Scedrov, A. (eds.), Categories in Computer Science and Logic. Contemporary Mathematics vol. 92, American Mathematical Society 63–66.CrossRefGoogle Scholar
Hyland, J. M. E. (2014). Elements of a theory of algebraic theories. Submitted to Theoretical Computer Science 546 132–144.Google Scholar
Hyland, M. (1976). A syntactic characterisation of the equality in some models of the lambda calculus. Journal of the London Mathematical Society 12 361–370.Google Scholar
Hyland, M. and Power, J. (2007). The category theoretic understanding of universal algebra: Lawvere theories and monads. In: Cardelli, L., Fiore, M. and Winskel, G. (eds.) Computation, Meaning and Logic. Articles Dedicated to Gordon Plotkin. Electronic Notes in Theoretical Computer Science 172 437–458.Google Scholar
Koymans, C. P. J. (1984). Models of the Lambda Calculus. Ph.D. thesis, Utrecht.Google Scholar
Lambek, J. (1980). From λ-calculus to cartesian closed categories. In: Seldin, J. P. and Hindley, J. R. (eds.), To H. B. Curry: Essays on Combinatory Logic and Formalism, Academic Press 375–402.Google Scholar
Lambek, J. and Scott, P. J. (1986). Introduction to Higher Order Categorical Logic, Cambridge University Press.Google Scholar
Lawvere, F. W. (1963). Functorial Semantics of Algebraic Theories, Ph.D. thesis, Columbia University. Republished with an introduction in Reprints in Theory and Applications of Categories 5 2004, 1–121.Google Scholar
Manzonetto, G. and Salibra, A. (2006). Boolean algebras for λ-calculus. In: Proceedings 21st Annual IEEE Symposium on Logic in Computer Science 317–326.Google Scholar
Scott, D. S. (1980) Relating theories of the λ-calculus. In: Seldin, J. P. and Hindley, J. R. (eds.), To H. B. Curry: Essays on Combinatory Logic and Formalism, Academic Press 403–450.Google Scholar
Selinger, P. (2002). The lambda calculus is algebraic. Journal of Functional Programming 12 549–566.Google Scholar
Tanaka, M. and Power, J. (2006). A unified category-theoretic semantics for binding signatures in substructural logics. Journal of Logic and Computation 16 5–25.Google Scholar
Taylor, P. (1986). Recursive Domains, Indexed Category Theory and Polymorphism, Ph.D. thesis, University of Cambridge.Google Scholar
Taylor, W. (1973). Characterizing Mal'cev conditions. Algebra Universalis 3 351–397.Google Scholar
Taylor, W. (1993) Abstract clone theory. In: Rosenberg, I. G. and Sabidussi, G. (eds.), Algebras and Orders, Springer 507–530.CrossRefGoogle Scholar