CPSC 417: Foundations of Functional Programming

Author: Robin Cockett
Date: 9th November 2005

Due:  29th November 2005

Assignment #3:  A type checker for the extended simply typed lambda calculus.

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:

Your program should allow you to input a term and it should respond with that term typed followed by the
normalized term typed.
The lab notes are here.