Go backward to Example Go up to Top Go forward to Soundness Theorem

Soundness of the Typing Rules.

Are the typing rules sensible in their assignment of type attributes to phrases?

• Typing rules must be sound.
  • Every well-typed program has a meaning.
• Type attributes:
  • T ::= int | bool
  • H ::= intloc | Texp | comm
• Mapping of attributes to meanings:
  • [[int]] = Int
  • [[bool]] = Bool
  • [[intloc]] = Location
  • [[Texp]] = Store -> [[T]]
  • [[comm]] = Store -> Store_bottom

How are [[P:H]] and [[H]] related?