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:
intexp
E:
realexp
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
Author:
Wolfgang Schreiner
Last Modification: March 26, 1998
