Semantics of the Core Language
Denotational semantics
 Recursively defined function.
 Mapping of a welltyped 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"
Author: Wolfgang Schreiner
Last Modification: March 26, 1998