Go backward to
Lazy Evaluation
Go up to
Top
Go forward to
Copy Rule
Soundness of Typing Rules
Type attributes
theta
::=
tau
|
tau
exp
|
comm
|
delta
|
delta
class
|
pi
dec
|
theta
1
->
theta
2
.
tau
::=
int
|
bool
delta
::=
intloc
|
pi
pi
::= {
j
:
theta
j
}
j in J
, J subset Identifier.
Lazy evaluation semantics:
[[
theta
1
->
theta
2
]] = [[
theta
1
]]
->
[[
theta
2
]]
Prove soundness of typing rules:
[[
pi
|- U:
theta
]] in Env
P
->
[[
theta
]]
[[
pi
|-
define
I
1
(I
2
:
theta
1
) = U: {I:
theta
2
}
dec
]]
e
in
[[{I
1
:
theta
1
->
theta
2
}
dec
]]
[[
pi
-U- {I
2
:
theta
1
} |- U:
theta
2
]](
e
-U-{I
2
=
v
}) in [[
theta
2
]]
for every
v
in [[
theta
1
]]
Eager evaluation semantics more complex:
[[
tau
exp
->
comm
]] = [[
tau
]]
->
[[
comm
]]
Author:
Wolfgang Schreiner
Last Modification: May 7, 1998