**Lecturer: Robin Cockett**

Why is functional programming important ....

- It promotes the view of programming as a mathematical
activity.

- 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
programming!

**COURSE OUTLINE:**

There will be a midterm exam and a final exam. The course will cover the following topics in roughly this order:

- 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 + assignment)
- Type checking and type inference (5 lectures + assignment)
- Strong normalization in the typed lambda calculus (2 lectures)

**READING (recommended):
**

- Benjamin Pierce "Types and Programming Languages" MIT Press.
- Graham Hutton "Programming in Haskell" Cambridge University
Press.

**LECTURE NOTES **(as they become available)**:**

- Introduction: functional programming, Haskell, and HUGS (includes the use of the state monad for substitution).
- Introduction to proofs in general.
- On the history of computability here.

- A programming approach to the lambda calculus:
- Paulson's notes, and some notes of mine - still in development - here
- Notes on reduction strategies here.
Slides for the modern SECD machine (by Prashant Kumar) here.

- A lambda calculus reducer by Sean Nichols here

- Notes on rewriting.
- The typed lambda calculus with fixed points.
- Course handout (a bunch of
useful papers).

- [Due September 26] Getting going with Haskell (8%) assignment 1.
- [Due October 24] Lambda lifting (14%) assignment 2.
- [Due November 21] Abstract machines: lambda calculus reduction (8%) assignment 3.
- [Due December] Type inference for the lambda calculus here (15%).

- Midterm exam (20%) -- early November: previous exams --
please note a different order of topics may have been covered --
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).

Please find the lab. notes (Cole Comfort) here.

**HASKELL LINKS:**

- The Haskell home page has many useful subsidiary links (in particular to the various HUGS systems which you can download) .... well worth a visit.
- The definitive text on the lambda calculus (the theory underlying functional programming) is written by Henk Barendregt: there is now a revised edition of the book.
- Here is the main Journal on Functional programming.
- Here is a guide to functional programming on the Web compiled by Philip Wadler who is a cool guy and has many interesting links on his home page. Check out functional programming in the real world. An example of an expository paper is "History of logic and programming languages", this is of special interest (to me!) as it points to the close link between proof theory and programming languages.
- The main conference in the area is "The International Conference on Functional Programming (ICFP)" . Of particular interest is the functional programming contest (here for example is the 2001 contest ) which is held each year.
- Paul Hudak's homepage.

- Stefan Klinger's "Don't Panic" guide
to IO Monads

- On the monad
laws.

- Dr. Seuss on Parser Monads: well some good fun for those who have kids (who are still kids)!
- Monadic parsing: Graham Hutton and Erik Meijer

- 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 Slonneger.
- Here is are of Barendregt's notes on functional programming and the lambda calculus.
- Claus Reinke's page on functional programming.
- Here is a lambda calculus reduction workbench written by Peter Sestoft. The reducer is written in Moscow ML and allows one to explore different reduction strategies.

**COMPUTABILITY LINKS:**

- For a proof that the halting problem is undecidable see here.