Go backward to Lazy Evaluation
Go up to Top
Go forward to Copy Rule
Soundness of Typing Rules
- Type attributes
- theta ::= tau | tauexp | comm
| delta | deltaclass | pidec
| theta theta.
- tau ::= int | bool
- delta ::= intloc | pi
- pi ::= {:theta},
J subset Identifier.
- Lazy evaluation semantics:
- [[theta theta]] = [[theta]]
[[theta]]
- Prove soundness of typing rules:
- [[pi |- U:theta]]
in Env [[theta]]
- [[pi |- define I(I:theta) = U:
{I:theta}dec]] in
[[{I:theta
theta}dec]]
- [[pi -U- {I: theta} |- U:theta]](
-U-{I=}) in [[theta]]
for every in [[theta]]
- Eager evaluation semantics more complex:
- [[tauexp comm]] = [[tau]]
[[comm]]
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: parameter.tex,v 1.1 1996/04/25 11:40:48 schreine Exp schreine