Go backward to
Lazy Evaluation
Go up to
Top
Go forward to
Soundness of Typing Rules
Lazy Evaluation
Invocation:
[[
pi
|-
call
I
1
(E):
comm
]]
e
s
=
p
f
s
where (I
1
=
p
) in
e
and
f s'
= [[
pi
|- E:
tau
exp
]]
e
s'
Formal parameter reference:
[[
pi
|- I
2
:
tau
exp
]]
e
s
=
f(s)
where (I
2
=
f
) in
e
Current store is supplied to formal parameter!
Author:
Wolfgang Schreiner
Last Modification: May 7, 1998