Go backward to Summary (Typing Rules V)
Go up to Top
Go forward to Summary (Semantics II)
Summary (Semantics I)
- Lazy evaluation semantics of abstractions:
- [[ |- define I=U: {I:}dec]]
= {I=},
where = [[ |- U:]] .
- [[ |- invoke I:]] = ,
where (I=) in .
- Recursively defined abstractions (example)
- [[ |- rec-proc I=C: {I:comm}dec]]
= ({I=}, )
where = [[ U {I:comm} |- C:comm]]
( union{I=}).
- Soundness of typing rules:
- [[ |- U:]] in
EnvP
[[]].
- Program
-
[[D in C: comm]] = [[ |- C:
comm]] ,
where (, ) = [[{} |- D: dec]]{}
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction2.tex,v 1.1 1996/04/10 07:30:13 schreine Exp schreine