Go backward to Proof Trees Go up to Top Go forward to Semantic Algebras

Semantics of the Core Language

Denotational semantics

• Recursively defined function.
  • Mapping of a well-typed derivation tree to its mathematical meaning.
• Semantic algebras.
  • Meaning sets (domains) and operations.
  • Bool, Int, Location, Store.
• For each typing rule, a recursive definition.

  • L: intloc	E: intexp
    L:=E: comm

    
    
  • [[L:=E: comm]] ...
    = ...[[L: intloc]] ...[[E: intexp]] ...
• Compositional semantic definitions.
  • Meaning of tree constructed from meanings of its subtrees.

Function [[.]] is read as "the meaning of"