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: