# McMaster University

CAS 706

#### Assignment 3

Typed Lambda-calculus interpreter.

Your term language should be based on:
var :== any sequence of lower case letters
int :== any integer
op1 :== - | not
op2 :== + | * | and | or | == | < | <=
term :== var | int | bool | Apply term term | Abs var term |
let var = term in term | op1 term | op2 term term |
if term then term else term fi

You should first write down the typing rules for your language.
You are allowed, even highly encouraged, to **improve** the above
grammar to make your life easier, so that typing rules can be made
simpler. Your task is to have your interpreter first *derive types*
for all inputs before any reduction is done. Error messages should be
returned for untypable terms. The interpreter should then proceed as in
assignment 2.
You should also be providing some test cases for
your interpreter - make sure to test higher-order functions as well as
cases that get do not type (ie old stuck cases from assignment 2) and
cases that work but are rejected in your typed
language.

In other words, you are writing a **type inference**
routine as the most important part of this assignment.

*Sept 2014*