CSE 340 HW 6

Due date: April 5, 2004
What to submit: A text file called lastname.txt containing the answers to the questions below, where lastname is replaced by your last name.

Proving type soundness

In this homework, you will extend the proof of type soundness that we talked about in class to a language with boolean values.

Consider an extension of the simply-typed language given in lecture that includes the boolean values true and false, the zero? primitive, and if. It also includes a new type "bool", and true and false are possible values of evaluation.

e ::= i | proc (t x) e | (e1 e2) | (e1 + e2) | true | false | if e1 then e2 else e3 | zero?(e) 
v ::= i | ProcVal(t,x,e,E) | true | false | RuntimeError
t ::= int | t1 -> t2 | bool

The following new rules describing the evaluation of these new terms (for convenience, each rule has a name in square brackets):

[true]

    (eval E true) = true
 

[false]

   (eval E false) = false


[if-true]

   (eval E e1) = true
   (eval E e2) = v
   ------------------
   (eval E (if e1 then e2 else e3)) = v 


[if-false]

   (eval E e1) = false
   (eval E e3) = v
   ------------------
   (eval E (if e1 then e2 else e3)) = v 


[zero?-zero]

    (eval E e1) = 0
   ------------------
   (eval E zero?(e1)) = true


[zero?-nonzero]

    (eval E e1) = i (not 0)
   --------------------------
   (eval E zero?(e1)) = false

Write the typing rules for these new constructs in the style of the lecture. The rules you write should correspond to the type-checker from Homework 5.

Add preconditions to the following two evaluation rules to propagate RuntimeError:

[if-wrong]
                ???????
   ------------------------------
   (eval E (if e1 then e2 else e3)) = RuntimeError
    
    
[zero?-wrong]

                ??????
   -------------------------------
    (eval E zero?(e)) = RuntimeError

What two new rules should we add for type checking values?
Extend the proof of type preservation to include cases for the rules [true], [if-true], and [if-wrong]