Sciweavers

Share
CADE
2003
Springer

adbmal

9 years 10 months ago
adbmal
We make the notion of scope in the -calculus explicit. To that end, the syntax of the -calculus is extended with an end-of-scope operator , matching the usual opening of a scope due to . Accordingly, -reduction is extended to the set of scoped -terms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped -reduction. Confluence of -reduction for the ordinary -calculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, -equivalence is needed. All our proofs have been verified in Coq.
Dimitri Hendriks, Vincent van Oostrom
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Dimitri Hendriks, Vincent van Oostrom
Comments (0)
books