Go backward to The Semantics of AbstractionsGo up to TopGo forward to Soundness Theorem |

Are typing rules and semantics well formed?

- Environment
*e*must be*consistent*with type assignment*p*- Calculation of [[
*p*|-U:*H*]]*e*.

- Calculation of [[
- Syntax of type attributes:
*H*::=*T*`exp`|`intloc`|`comm`|*p*`dec`.*T*::=`int`|`bool`.*p*::= {i:*H*}_{i}, where I subset of Identifier._{i}in I

- Meaning of type attributes:
- [[
*T*`exp`]] =`Store`*->*[[*T*]]. - [[
`intloc`]] =`Location`. - [[
`comm`]] =`Store`*->*`Store`._{b}ottom - [[
*p*`dec`]] =`Store`*->*[[*p*]]. - [[
`int`]] =`Int`. - [[
`bool`]] =`Bool`. - [[{
*i*:*H*}_{i}]] = {_{i}in I*i*:[[*H*]]}_{i}_{i}in I

(set of environments {I=_{1}*v*,...,I_{1}=_{n}*v*})._{n}

- [[

Author: Wolfgang Schreiner

Last Modification: April 2, 1998