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:H_i}_i in I, where
I subset of Identifier.
- Meaning of type attributes:
- [[Texp]] = Store -> [[T]].
- [[intloc]] = Location.
- [[comm]] = Store ->
Store_bottom.
- [[pdec]] = Store -> [[p]].
- [[int]] = Int.
- [[bool]] = Bool.
- [[{i:H_i}_i in I]] =
{i:[[H_i]]}_i in I
(set of environments {I_1=v_1,...,I_n=v_n}).
