Lecture notes on the lambda calculus

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. 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, type inference, denotational semantics, complete partial orders, and the language PCF. Contents

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Peter Selinger
• Keywords: CORR 2008, Education, Lambda Calculus, Simply-typed Lambda Calculus, Untyped Lambda Calculus