Go backward to
Summary (Typing Rules)
Go up to
Top
Go forward to
Summary (Lambda Abstraction)
Summary (Semantics)
Lazy evaluation semantics:
[[
pi
|-
define
I
1
(I
2
:
tau
exp
) =
U: {I
1
:
tau
exp
->
theta
}
dec
]]
e
s
= ({I
1
=
p
},
s
)
where
p
f
s
= [[
pi
-U- {I
2
:
theta
1
} |- U:
theta
2
]](
e
-U- {I
2
=
f
})
s
[[
pi
|-
invoke
I
1
(V):
theta
2
]]
e
s
=
p
f
s
where (I
1
=
p
) in
e
and
f
s'
= [[
pi
|- V:
theta
1
]]
e
s'
[[
pi
|- I
2
:
theta
]]
e
s
=
f
(
s
)
where (I
2
=
f
) in
e
Author:
Wolfgang Schreiner
Last Modification: May 7, 1998