McMaster University
CAS 706

Assignment 3

Typed Lambda-calculus interpreter. To be done in the same languages as assignment 2, except that you must "changed" one of them. Due: March 24th.
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.


Mar 2005