assignment 3

CPSC 521: Foundations of Functional Programming

Author: Robin Cockett
Date: 17th November 2008

Due: 5th December 2008

Assignment #4: 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 example program for unifying terms is here), 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 the 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 pretty printer for lambda calculus terms.
A pretty printer for the types of the calculus.
A term normalizer for these terms.

Your program should allow you to set up tests for raw terms the program should respond with that term typed followed by the normalized result term typed.