This is a set of lecture notes for the course “Mathematical Foundations of Computation”, which I taught at the University of Ottawa in Fall 2001. Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, type inference, denotational semantics, complete partial orders, and the language PCF.