Go backward to Soundness of the Typing RulesGo up to TopGo forward to Lazy Evaluation and Copy Rule |

- Consistency:
- Environment
*e*is`consistent`with type assignment*p*if (I:*H*) in*p*iff (I=*v*) in*e*and*v*in [[*H*]].

- Environment
- Soundness Theorem:
- If
*p*|- U:*H*and*e*consistent with*p*, then [[*p*|- U:*H*]]*e*in [[*H*]].

- If
- Proof: by structural induction on set of typing rules.
- For
*p*|-L:=E:`comm`, typing rule demands*p*|- L:`intloc`and*p*|-E:`intexp`. By inductive hypothesis, [[*p*|- L:`intloc`]]*e*in`Location`and [[*p*|- E:`intexp`]]*e*in`Store`*->*`Int`for*e*consistent with*p*. Hence, [[*p*|- L:=E:`comm`]]*e**s*=`update`([[*p*|- L:`intloc`]]*e*, [[*p*|- E:`intexp`]]*e**s*,*s*) in`Store`, implying [[*p*|- L:=E:`comm`]]*e*in`Store`*->*`Store`._{b}ottom

- For

*The typing rules of the extended core language are sound.*

Author: Wolfgang Schreiner

Last Modification: April 2, 1998