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)
    • Journal version: Berger, Eberl, Schwichtenberg, 2003: Term rewriting for normalization by evaluation (doi)
    • Original NbE paper: Berger & Schwichtenberg, 1991: An inverse of the evaluation functional for typed lambda-calculus (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
    • Schwichtenberg’s Minlog interactive proof system
    • Aehlig et al, 2008: A compiled implementation of normalization by evaluation (doi, pdf)

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

  • Di Cosmo, 1995: Isomorphism of types: From lambda calculus to information retrieval and language design
  • Di Cosmo, 2005: A short survey of isomorphism of types (doi, pdf)
  • Fiore, Di Cosmo, Balat, 2006: Remarks on isomorphisms in typed lambda calculi with empty and sum types (doi, pdf)