Soundness of the Typing Rules
Are typing rules and semantics well formed?
- Environment e must be consistent with type assignment p
- Calculation of [[p |-U:H]]e.
- Syntax of type attributes:
- H ::= Texp | intloc | comm
| pdec.
- T ::= int | bool.
- p ::= {i:Hi}i in I, where
I subset of Identifier.
- Meaning of type attributes:
- [[Texp]] = Store -> [[T]].
- [[intloc]] = Location.
- [[comm]] = Store ->
Storebottom.
- [[pdec]] = Store -> [[p]].
- [[int]] = Int.
- [[bool]] = Bool.
- [[{i:Hi}i in I]] =
{i:[[Hi]]}i in I
(set of environments {I1=v1,...,In=vn}).
Author: Wolfgang Schreiner
Last Modification: April 2, 1998