PCES PI Meeting
Feb 2001
26
Expression Types Continued
•Elimination
rule (destructor)
•D ; G |- M : A D,u::A ; G |- N : C
•D ; G |- (let box u = M in N) : C
•Operational
semantics captures staging
•
M Þ box
E [E/u] N Þ V
•box E Þ
box E let box u = M in N Þ V
