Lecture notes on the lambda calculus

Abstract

This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007 and 2013. Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, polymorphism, type inference, denotational semantics, complete partial orders, and the language PCF.

120 pages. Added in v2: section on polymorphism

Cited by in corpus (7)

• Physics, Topology, Logic and Computation: A Rosetta Stone
• Knowledge Representation in Bicategories of Relations
• Teaching machines to understand data science code by semantic enrichment of dataflow graphs
• Logic and linear algebra: an introduction
• Signatures and models for syntax and operational semantics in the presence of variable binding
• Type-driven Neural Programming by Example
• On Coupled Logical Bisimulation for the Lambda-Calculus