Author: Robin Cockett
Date: 9th November 2005

Due:  29th November 2005

The main requirement of this assignment is to develop a type checker for the simply typed lambda calculus with fixed points, pairs, natural numbers, and lists : I call this the Basic Programming Language (BPL).   To achieve this you will need to have an implementation of the unification algorithm, an implementation of the type checking rules so that you can collect the type equations and solve them incrementally, and input and output routines so you can input a lambda calculus term and display its inferred type.  In addition, you should provide a term normalizer for this calculus using the rewrite rules supplied.

This extension to the simpy typed lambda calculus (BPL) is described here.

The deliverables for this assignment are:

• A parser for extented lambda calculus terms.
• A pretty printer for lambda calculus terms.
• A pretty printer for the types of the calculus.
• A term normalizer for these terms.