Go backward to
Typing Rules Define a Language
Go up to
Top
Go forward to
Semantics of the Core Language
Proof Trees
Programs may be directly derived from typing rules.
Typing rules form a
logic
.
Set of axioms and inference rules.
(Inverted) trees are logic
proof trees
.
Author:
Wolfgang Schreiner
Last Modification: March 26, 1998