CPSC 521: Foundations of Functional Programming

Author: Robin Cockett
Date: 2nd December 2014

Due:  12th December midnight

Assignment #4:  Type inference for BPCF.

The main requirement of this assignment is to develop a type inference algorithm for the simply typed lambda calculus with fixed points, pairs, natural numbers, and lists: I call this the Basic Programming language for Computable Functions (BPCF).   To achieve this you will need to collect the type equations and to solve them incrementally.  In addition, as an optional extra you can arrange for programs applied to values to be evaluated on the modern SECD machine.

This extension to the simply typed lambda calculus (BPCF): it is described here together with the type inference algorithm.

The deliverables for this assignment are:

Your program (minimally) should allow you to determine whether a program is well-typed and display the program's most general type.   In order to run a program, you should arrange that defined programs can be applied to inputs.