Lecture notes on the lambda calculus
Logic in Computer Science
2013-12-30 v2
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.
Cite
@article{arxiv.0804.3434,
title = {Lecture notes on the lambda calculus},
author = {Peter Selinger},
journal= {arXiv preprint arXiv:0804.3434},
year = {2013}
}
Comments
120 pages. Added in v2: section on polymorphism