Homework # 5
due October 11

Reading

Please read Chapters 9 and 10 in the textbook.

Problems

Do the proof of Theorem 9.3.9 by induction over the derivation of the evaluation fact. (You may assume the preservation Lemma 9.3.8)

Discussion

In class, we discussed several dubious type rules. In particular, we discussed something similar the following system: \begin{mathpar}
\inferrule[T-Var]{ }{x : T}
\par\inferrule[T-Abs]{t : T}{\lambda...
...par\textrm{\ldots additional rules for booleans and \lq\lq if'' \ldots}
\end{mathpar} Suppose we try to prove progress and preservation with this ``type system.'' Can we do it? Explain! Give concrete examples.

If we changed the rules to \begin{mathpar}
\inferrule[T-Var]{ }{x : \texttt{Bool}}
\par\inferrule[T-Abs]{t ...
...par\textrm{\ldots additional rules for booleans and \lq\lq if'' \ldots}
\end{mathpar} Can we prove progress and preservation? Discuss!

Program Design

Consider rewriting the type checker to implement the first set of bad type rules. There is an implementation problem. How would you solve the problem?

About this document



John Tang Boyland
2005-10-04