Abstracts.2020.STLCCC

Simply-Typed λ-Calculus and Cartesian Closed Categories

by Andreas Abel and Sandro Stucki

Two-part lecture series scheduled for Nov 5 and 12, 2020. Previously held in three parts.

Part I: Simply-Typed λ-Calculus

• Recapitulation of simply-typed λ-calculus (STLC) with products and unit
• Explicit substitutions
• Equational theory for STLC with products, unit, and explicit substitutions
• Nameless presentation (de Bruijn style)
• Reduce de Bruijn indices to weakenings of the first de Bruijn index
• Show that the set of terms Γ ⊢ t : A is in bijection with substitutions Γ ⊢ σ : ε.A, but also with functions ε ⊢ f : ΠΓ → A where ΠΓ is the left-associated iterated product of Γ. The point is that the judgement of t is asymmetric while the judgements of σ and f are symmetric, a pair of σ₁ and σ₂ or a pair of f₁ and f₂ may be composed.

Part II: Cartesian Closed Categories

• Categories: basic definition
• Cartesian closed categories (CCCs) with a choice of
  • Terminal objects
  • Binary products
  • Exponential objects
• The internal language of CCCs
• Implementing the internal language of CCCs in STLC with products

Notes, Exercises and Code

• Lecture notes and exercises
• Agda code

Literature

Reading on this lecture:

• Wikipedia, Curry-Howard-Lambek-Correspondence
• Andreas Abel, Lambda-Kalkül, Kapitel 7 (7.0, 7.3, 7.4) und 9 (9.0, 9.1, 9.3, 9.4) (in German)
• Jonathan Prieto-Cubides, The Simply Typed Lambda Calculus, slides: From named terms to de Bruijn terms; type-checking. Based on Agda code by gergoerdi
• Steve Awodey, Category theory, Section 6.6
• Joachim Lambek and Philip J. Scott, Introduction to higher order categorical logic

Further reading on categorical logic of simply-typed λ-calculus:

• Simon Castellan and Pierre Clairambault and Peter Dybjer, Categories with Families: Unityped, Simply Typed, and Dependently Typed, Section 4

Further reading on λ-calculus:

• Peter Selinger, Lecture Notes on the Lambda Calculus
• Ralph Loader, Notes on Simply Typed Lambda Calculus