Go backward to Soundness of the Typing Rules
Go up to Top
Go forward to Lazy Evaluation and Copy Rule
Soundness Theorem
- Consistency:
- 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 ->
Store_bottom.
The typing rules of the extended core language are sound.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine