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"
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine