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 lambda calculus with products and sums, and go on to cover two different extensions of this calculus, one with a monad and another with a box modality.
Bring pen and paper!
Coming up!
Coming up!