Go backward to
The Semantics of Abstractions
Go up to
Top
Go forward to
Soundness of the Typing Rules
The Semantics of Abstractions
Expression: [[E:
T
exp
]] in
Environment
->
Store
->
[[
T
]]
[[
p
|- N:
intexp
]]
e
s
= [[
p
|- N:
int
]]
e
[[
p
|- @L:
intexp
]]
e
s
=
lookup
([[
p
|-L:
intloc
]]
e
,
s
)
[[
p
|- E
1
+E
2
:
intexp
]]
e
s
=
plus
(
[[
p
|- E
1
:
intexp
]]
e
s
, [[
p
|- E
2
:
intexp
]]
e
s
)
[[
p
|- E
1
=E
2
:
boolexp
]]
e
s
=
equal
(
[[
p
|- E
1
:
intexp
]]
e
s
, [[
p
|- E
2
:
intexp
]]
e
s
)
[[
p
|-
not
E:
boolexp
]]
e
s
=
not
([[
p
|- E:
boolexp
]]
e
s
)
[[
p
|- I:
T
exp
]]
e
s
, where (I=
v
) in
e
Location: [[L:
intloc
]] in
Environment
->
Location
[[
p
|-
loc
i
:
intloc
]]
e
=
loc
i
Numeral: [[N:
int
]] in
Environment
->
Int
[[
p
|-
n
:
int
]]
e
=
n
Author:
Wolfgang Schreiner
Last Modification: April 2, 1998