- Environment e is consistent with type assignment p if
(I:H) in p iff (I=v) in e and v in [[H]].
- Soundness Theorem:
- If p |- U:H and e
consistent with p, then [[p |- U:H]]e in [[H]].
- 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 ->
The typing rules of the extended core language are sound.
Author: Wolfgang Schreiner
Last Modification: April 2, 1998