Abstracts.2017.STLCCC

Simply-typed lambda-calculus and cartesian closed categories

by Andreas Abel

Lecture scheduled for Thu, 30 Nov 2017.

Part 1: Lambda-calculus

• Recapitulation of simply-typed lambda-calculus (STLC)
• Explicit substitutions
• Equational theory for STLC with explicit substitutions
• Nameless presentation (de Bruijn style)
• Agda-implementation of STLC

Part 2: Categories

• Categories: basic definition
• Cartesian closed categories (CCCs)
  • Unit type (terminal object)
  • Product type (product object)
  • Function type (exponential object)
• The internal language of CCCs
• Agda-implementation of this internal language

Part 3: The connection

• Interpreting STLC in CCCs
• STLC with products
• Implementing the internal language of CCCs in STLC with products

Exercises

Exercises

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 typed lambda-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

Further reading on lambda-calculus:

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