Go backward to Unicity of Typing
Go up to Top
Go forward to Proof Trees
Typing Rules Define a Language
- Typing rules (not abstract syntax) define language.
- Only well-formed programs are of value.
- Programs are well-typed trees.
- Significance of unicity of typing:
- Linear representation without type annotations represents (at most) one
program.
- Example: 0+1.
- Without unicity of typing:
- Coherence: different tree derivations of a linear representation
should have same meaning.
-
E_1:realexp | E_2:realexp |
E_1+E_2:realexp
|
- (((0)^int+(1)^int)^intexp)^realexp.
- ((((0)^int)^intexp)^realexp +
(((1)^int)^intexp)^realexp)^realexp
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: core.tex,v 1.3 1996/02/05 10:34:52 schreine Exp schreine