Classical lambda calculus in modern dress
Martin Hyland
TL;DR
This paper explores the lambda calculus through the lens of categorical logic, providing new insights and simplified proofs for its semantics based on recent advances in categorical foundations of algebra.
Contribution
It introduces a categorical interpretation of lambda calculus as semi-closed algebraic theories, offering a natural and precise understanding aligned with Scott's representation theorem.
Findings
Categorical interpretation of lambda calculus as semi-closed algebraic theory
Simplified proofs of fundamental semantic results
Establishment of equivalence with traditional notions
Abstract
Recent developments in the categorical foundations of universal algebra have given fresh 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 precise theorems showing the essential equivalence with more familiar notions. Simple abstract proofs of fundamental results in the semantics of the lambda calculus are given.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.