Abstracts.2021.STLCCC

Simply-Typed λ-Calculus and Cartesian Closed Categories

by Sandro Stucki and Andreas Abel

Three-part lecture series scheduled for Sep 16 and 23 and 30, 2021.

Part I: Simply-Typed λ-Calculus

Lecture given by Sandro Stucki.

• Recapitulation of simply-typed λ-calculus (STLC) with named bound variables, judgements Γ ⊢, ⊢ A, Γ ⊢ t : A, Γ ⊢ t = u : A, and function types A → B
• Internalization of substitutions as terms by adding judgements Δ ⊢ σ : Γ, Δ ⊢ σ = τ : Γ and explicit substitutions Δ ⊢ t ∘ σ : A
• Nameless representation of bound variables (de Bruijn style)
• Reduction of de Bruijn indices n to weakenings 0 ∘ pⁿ of the first de Bruijn index 0 by adding substitutions Γ, A ⊢ p : Γ
• Internalization of contexts as types by adding unit and product types 1 and A × B

Part II: Cartesian Closed Categories

Lecture given by Andreas Abel.

• Categories: Basic definition and structures of the algebra of functions
• Cartesian closed categories (CCCs) 𝒞 with a choice of
  • Terminal object 1 : 1 → 𝒞
  • Binary products -×- : 𝒞 × 𝒞 → 𝒞
  • Exponential/internal hom objects -A : 𝒞 → 𝒞 for each A : 𝒞

Part III: Formalization of the two theories and the statement of their correspondence (TBA)

Slides, Notes, Exercises and Code

• Slides:

  • Part I

• Lecture notes and exercises:

  • Part II

• Code:

  • An Agda mechanization of the lectures
  • The agda-categories library contains Agda versions of most of the definitions, examples and exercises covered in the second lecture

Literature

Reading on this lecture:

• Wikipedia, Curry–Howard–Lambek-Correspondence
• Martín Abadi, Luca Cardelli, Pierre-Louis Curien and Jean-Jacques Lévy, Explicit Substitutions (aka the λσ-calculus)
• 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 typed λ-calculus:

• Simon Castellan and Pierre Clairambault and Peter Dybjer, Categories with Families: Unityped, Simply Typed, and Dependently Typed, see Section 4 for the simply-typed case
• nLab, Closed Cartesian multicategories

Further reading on λ-calculus:

• Peter Selinger, Lecture Notes on the Lambda Calculus
• Ralph Loader, Notes on Simply Typed Lambda Calculus
• Paul Blain Levy, Typed λ-calculus: course notes

Related talks:

• Andreas, Simply-typed lambda-calculus and cartesian closed categories
• Nachi, Categorical Combinators
• Andreas and Sandro, Simply-Typed λ-Calculus and Cartesian Closed Categories