CMSC 221/321
Homework set 4
Due: Tuesday, Nov 9, 2010

4.1. Verify that fact = Yv Fact defines the factorial in CBV semantics
by hand calculating (fact 2) (using Fun[SSv] rules).  Follow the
example of the calculation of (fact 2) using the CBN Y combinator in
Lecture 6.


4.2. Write out the derivation of the typing judgement

    ⊦ let x: Int → Int = λy:Int.y+1 in x(3) : Int

(after translating the expression into TFun abstract syntax).


4.3. Give a full and rigorous proof of the Substitution Lemma
(Lemma 4.9), using the proof of the Substitution Lemma for the ok
judgement (Lemma 4.4, Lecture 7) as the template.


4.4. Write a type checker in SML for the TFun language. This will be
a function that takes an expression e and a type environment Γ and
produces a type τ such that Γ ⊦ e: τ.  You will need to define types
for the abstract syntax of expressions and types, and for typing
environments (use an association list).  You will also need to 
implement a mapping (Σ) from constants to their types representing the
"signature" of the language.

  type variable
  type const
  type expr
  type ty
  type tyenv = (variable * ty) list

The main function will have the following type:

  val typeOf: expr * tyenv -> ty