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

Soundness Theorem

[[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]].
• Case C₁;C₂: comm
  • We know [[C₁: comm]] and [[C₂: comm]] are elements of Store -> Store_bottom. For every Store s, we have [[C₁;C₂: comm]](s) = [[C₂: comm]]([[C₁: comm]](s)) and [[C₂:comm]](s) = s₁ in Store_bottom. If s₁=bottom, [[C₂: comm]](s₁)=bottom in Store_bottom. If s₁ in Store, then [[C₂: comm]](s₁) in Store_bottom. Hence, [[C₁;C₂: comm]] in Store -> Store_bottom = [[comm]].

Prove one case for each typing rule.