Lecture Notes on the Lambda Calculus Peter Selinger DDaihouremde Abstract Topics de the lambda caleulutheCurry-Howrd isomorism. Contents 1 Introduction 4 1.1 Extensional vs.intensional view of functions 1.2 The lambda calculus 6 1.3 Untyped vs.typed lambda-calculi 7 1.4 Lambda calculus and computability............. 1.5 Connections to computer science..................9 1.6 Connections to logic 9 1.7 Connections to mathematics....................10 2 The untyped lambda calculus 2.1 Syntax. Lecture Notes on the Lambda Calculus Peter Selinger Department of Mathematics and Statistics Dalhousie University, Halifax, Canada 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. 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 normal￾ization, type inference, denotational semantics, complete partial orders, and the language PCF. Contents 1 Introduction 4 1.1 Extensional vs. intensional view of functions . . . . . . . . . . . 4 1.2 The lambda calculus . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Untyped vs. typed lambda-calculi . . . . . . . . . . . . . . . . . 7 1.4 Lambda calculus and computability . . . . . . . . . . . . . . . . 8 1.5 Connections to computer science . . . . . . . . . . . . . . . . . . 9 1.6 Connections to logic . . . . . . . . . . . . . . . . . . . . . . . . 9 1.7 Connections to mathematics . . . . . . . . . . . . . . . . . . . . 10 2 The untyped lambda calculus 10 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1