Introduction to Types and Lambdas

Held at SPLV ‘26 (event).

Abstract

Types were introduced to me as a restriction bolted on top of the untyped lambda calculus to prevent certain runtime errors. Shackles I must program with, because I cannot be trusted with the power of the unruly lambda calculus. In this course, I will present types through the lens of a different paradigm, where types are internalized into the definition of the calculus and terms are well-typed (thus free of said errors) by construction. This view of types, sometimes called an intrinsic view, aligns naturally with proof theory and is incredibly well suited for mechanization and mathematical treatment.

The objective of this course is to provide an introduction to typed lambda calculi and their denotational semantics by means of well-typed interpreters. We will begin with a simply typed program calculus with products and sums, and go on to cover three different extensions of this calculus, namely with lambdas, a monad and a “box” modality.

Bring pen and paper!

Lectures

1. A calculus with sums and products

   • Types, contexts and well-typed terms
   • Detours, conversions and admissibility
   • Terms as functions on sets
   • Evaluating closed terms
   • Evaluating open terms?

2. Normalisation by Evaluation

   • Normal forms and the subformula property
   • Terms as functions on families of sets
   • Failure of reflection and covering families
   • Reification and reflection
   • Examples of normalisation in action

3. Lambdas, monads & boxes

   • Examples of normalisation in action
   • Functions and lambdas, finally!
   • Monads and Moggi’s monadic metalanguage
   • Box modalities and a Fitch-style modal calculus
   • Things I wish we had time for
   • Things we had time for

Supplementary material

Lecture 1:

• slides

Lecture 2:

• slides
• browse code
• download code

Lecture 3:

• slides
• browse code
• download code

Related courses

Other courses at SPLV ‘26 related to this one are: Introduction to Category Theory by Bob Atkey, Algebra and Normalisation by Ohad Kammar (course page), and Highly-Assured Programming Language Design and Implementation using Dependent Types by Jan de Muijnck-Hughes (course page). If you have the capacity to travel back in time, I recommend The lambda calculus, formalised: the Church-Rosser and Standardisation theorems, with applications by James McKinna at SPLV ‘22 (event, recordings).

References

Lecture notes:

• Brief Notes on the Category Theoretic Semantics of Simply Typed Lambda Calculus by Andrew Pitts (2017) (url)
• Normalization by Evaluation for Intuitionistic Propositional Logic by Andreas Abel (2018) (url)
• Lambda Calculus and Combinatory Algebra by Sam L. Speight (2026) (url)

Textbooks:

• Basic Proof Theory (Second Edition) by A. S. Troelstra and H. Schwichtenberg (2000)
• Proof and Types by J. Y. Girard (1989), translated by Paul Taylor and Yves La Font (2003) (url)

Research articles:

• Notions of computations and monads by Eugenio Moggi (1991) (doi)
• Extensional Rewriting with Sums by Sam Lindley (2007) (doi)
• Fitch-Style Modal Lambda Calculi by Ranald Clouston (2018) (doi)
• Normalization for Fitch-Style Modal Calculi by Nachi Valliappan, Fabian Ruch and Carlos Tomé Cortiñas (2023) (doi)
• Lax Modal Lambda Calculi by Nachi Valliappan (2026) (doi)