Skip to content

Abstracts.2020.STLCCC

Jump to bottom
Fabian edited this page Nov 3, 2020 · 27 revisions

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 product A × B and unit 1 types
  • Explicit substitutions Δ ⊢ t ∘ σ : A for Γ ⊢ t : A and Δ ⊢ σ : Γ
  • Equational theory Γ ⊢ t = u : A for STLC with product and unit types, and explicit substitutions. The point is that substitution was defined by inspection of the syntax of terms but is now axiomatized.
  • Nameless presentation (de Bruijn style)
  • Reduce de Bruijn indices n to weakenings 0 ∘ pⁿ of the first de Bruijn index 0
  • 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 type of Γ ::= ε | Γ.A. 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 of the algebra of functions
  • Cartesian closed categories (CCCs) with a choice of
    • Terminal object
    • Binary products
    • Exponential/internal hom objects
  • The internal language of a CCC
  • Implementing the internal language of a CCC in STLC with product and unit types

Notes, Exercises and Code

Literature

Reading on this lecture:

Further reading on categorical logic of typed λ-calculus:

Further reading on λ-calculus:

Clone this wiki locally