Skip to content

Abstracts.2020.STLCCC

Jump to bottom
Andreas Abel edited this page Nov 12, 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 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

  • Categories: Basic definition 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 : 𝒞

    Note that each of these three categorical structures can be defined as "the" right adjoint to a previously defined functor, and thus both by a universal property but also purely equationally.

  • The internal language of a CCC

  • Implementing the internal language of a CCC in STLC with product and unit types

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