![\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}](homework5-img1.gif)
Suppose we try to prove progress and preservation with this ``type system.''
Can we do it? Explain! Give concrete examples.
Please read Chapters 9 and 10 in the textbook.
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)
In class, we discussed several dubious type rules. In particular, we
discussed something similar the following system:
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}](homework5-img2.gif)
Can we prove progress and preservation? Discuss!
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?