Lambda calculus
The typed lambda calculus (with fixed point operator) is a fundamental model of computation and a hallmark of programming language theory.
Literature
General references
- Selinger, 2013: Lecture Notes on the Lambda Calculus (arxiv)
- Gunter, 1992: Semantics of Programming Languages, Ch 3. Categorical models
of simple types
- Clear introduction to lambda calculus and its categorical models
Subtypes
See also category-theoretic references
- Mitchell, 1996: Foundations of Programming Languages, Ch. 10: Subtyping and
related concepts
- Sec 10.2: Simply typed lambda calculus with subtypes
- Sec 10.3: Records [as extension of subtype calculus]
Normalization by evaluation (NbE)
Main approach to computer algebra/theorem proving for lambda calculus (see my CS.SE question ).
- Berger, Eberl, Schwichtenberg, 1998: Normalization by evaluation (doi)
- Categorical interpretations
- Cubric, Dybjer, Scott, 1998: Normalization and the Yoneda embedding (doi)
- Dybjer’s lecture notes on NBE and Yoneda for monoids
- Altenkirch et al, 2001: Normalization by evaluation for typed lambda calculus with coproducts (doi, pdf) (commentary on CS.SE)
- Implementations
Higher-order unification: unification with function variables
- Dowek, 2001: Higher-order unification and matching (Ch. 16 in Handbook of Automated Reasoning) (doi)
- Huet & Lang, 1978: Proving and applying program transformations expressed with second-order patterns (doi)
Type equality and isomorphism