Exercise Session 06

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) $f(false ? true : false)$

b) $\lambda x: boolean. f(x ? false : x) $

The initial environment contains the following types: $f: boolean \rightarrow boolean, true: boolean, false: boolean$

3) Find an environment $\Gamma$ under which the term $f x y$ gas type $boolean$.