This summarizes activities done in class on 22 October 2008.

Type checking and evaluation for simply typed lambda calculus

Solved exercises:

1) Prove that the following program is type correct:

class Max {
  int max (int x, int y) {
    int res;
    res = (x > y) ? x : y;
    return res;
  }
}

2) Type check the following simply typed lambda terms:

a)

b)

The initial environment contains the following types:

3) Find an environment under which the term gas type .