CPSC521: FOUNDATIONS OF FUNCTIONAL PROGRAMMING
(Winter 2022, ST 127, TuTh 3:30pm-4:45pm -- initially on-line)
Lecturer: Robin Cockett
The purpose of the course is to explore various aspects of
functional programming using Haskell. In particular, the
course provides an introduction to the lambda calculus, abstract
machines, types in programming, type inference, and the role of
these in the implementation of functional programming.
Why is functional programming matters ....
- It promotes the view of programming as a mathematical
- It promotes programming abstractions (generic code).
- It is typed .... the Hindley-Milner polymorphic type checker.
- It allows fast accurate
prototyping for complex programs.
- It has datatypes, classes, monads, and many other goodies.
- It helps you, the programmer, develop a clear view of
There will be a midterm exam and a final exam. The course
will cover the following topics in roughly this order:
- Revision of/Introduction to data, maps, and folds in Haskell
(3 lectures + assignment)
- Monads, classes, and other topics (3 lectures + assignment)
- Introduction to the lambda calculus (5 lectures)
- Introduction to abstract machines and/or rewriting (2 lectures
- Type checking and type inference (5 lectures + assignment)
- Strong normalization in the typed lambda calculus (2 lectures)
- Benjamin Pierce "Types and Programming Languages" MIT Press.
- Graham Hutton "Programming in Haskell" Cambridge University
- Miran Lipovaca "Learn you a Haskell for the greater good" here.
- Roger Hindley and Jonathan Seldin "Lambda-Calculus and
combinators an introduction".
LECTURE NOTES (as they become available):
- [Due January 28]
Getting going with Haskell (8%) assignment
1 (template file is here with types)
- [Due March 4] Lambda
lifting (14%) assignment
2 (hint: here
is some example code for \alpha renaming lambda expressions).
- [Due March 25]
Abstract machines: lambda calculus reduction (8%) assignment 3.
- [Due April 12]
Type inference for the lambda calculus here (15%).
GRADESCOPE AND ZOOM:
- Midterm exam (20%) -- on the 17th March: previous exams --
please note a different order of topics may have been covered --
2020, 2016, 2014,2010, 2009, 2007, 2006 and exercise sheet, 2005 and answers, 2002.
- Final exam (35%), (previous finals 2002, 2006, 2007, and 2008 oral, 2014, 2016).
The course will use gradescope for grading assignments and
exams. Students need to sign up at gradescope.ca (press the
"sign up" button). To find the course entry code, go to the
course in D2L and pull down the "content" tab. The zoom links
for the on-line portions of the course will be here.
Please find the lab. notes (Haiyang He and Jared Pon).
LAMBDA CALCULUS AND FUNCTIONAL
- John Harrison's notes
on functional programming.
- Larry Paulson's notes on a
programming approach to the lambda calculus.
- A basic
introduction to the untyped Lambda Calculus by Ken
- Here are Barendregt's notes
on functional programming and the lambda calculus.
- Claus Reinke's page
on functional programming.
- Here is a lambda
reduction workbench written by Peter Sestoft. The reducer
is written in Moscow
ML and allows one to explore different reduction
- For a proof that the halting problem is undecidable see here.