Go backward to Soundness of the Typing Rules.Go up to TopGo forward to Operational Properties |

[[P:*H*]] in [[*H*]], for
every well-typed phrase P:*H*

**Case***n*:`int`- [[
*n*:`int`]] =*n*in`Int`= [[`int`]]

- [[
**Case**@L:`intexp`- We know [[L:
`intloc`]] =*l*in [[`intloc`]] =`Location`. Then, for every Store*s*, [[@L:`intexp`]](*s*) =`lookup`(*l*,*s*) in`Int`i.e. [[@L:`intexp`]] in`Store`*->*`Int`= [[`intexp`]].

- We know [[L:
**Case**C;C_{1}:_{2}`comm`- We know [[C
:_{1}`comm`]] and [[C:_{2}`comm`]] are elements of Store*->*Store. For every Store_{b}ottom*s*, we have [[C;C_{1}:_{2}`comm`]](*s*) = [[C:_{2}`comm`]]([[C:_{1}`comm`]](*s*)) and [[C:_{2}`comm`]](*s*) =*s*in_{1}`Store`. If_{b}ottom*s*=_{1}*bottom*, [[C:_{2}`comm`]](*s*)=_{1}*bottom*in`Store`. If_{b}ottom*s*in_{1}`Store`, then [[C:_{2}`comm`]](*s*) in_{1}`Store`. Hence, [[C_{b}ottom;C_{1}:_{2}`comm`]] in`Store`*->*`Store`= [[_{b}ottom`comm`]].

- We know [[C

*Prove one case for each typing rule.*

Author: Wolfgang Schreiner

Last Modification: March 26, 1998