Skip to content

Abstracts.2021.STLCCC

Jump to bottom
Sandro Stucki edited this page Sep 17, 2021 · 8 revisions

Simply-Typed λ-Calculus and Cartesian Closed Categories

by Sandro Stucki

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

Part I: Simply-Typed λ-Calculus

  • 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 (TBA)

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

Slides, Notes, Exercises and Code

Literature

Reading on this lecture:

Further reading on categorical logic of typed λ-calculus:

Further reading on λ-calculus:

Related talks:

Clone this wiki locally