User loginNavigation 
adbmaL
... or how is the title of this paper pronounced?
We make the notion of scope in the lambdacalculus explicit. To that end, the syntax of the lambdacalculus is extended with an endofscope operator [adbmal], matching the usual opening of a scope due to lambda. Accordingly, betareduction is extended to the set of scoped lambdaterms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped betareduction. Confluence of betareduction for the ordinary lambdacalculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, alphaequivalence is needed. All our proofs have been verified in Coq.While playing with my own lambdamachine (derivative of CEK in Java) I decided that I would like to control scope better  so I found this paper. See also Lambdascope previously mentioned on LtU. 
Browse archives
Active forum topics

Recent comments
2 weeks 23 hours ago
2 weeks 5 days ago
2 weeks 6 days ago
2 weeks 6 days ago
3 weeks 5 days ago
4 weeks 1 day ago
4 weeks 1 day ago
4 weeks 1 day ago
5 weeks 3 days ago
5 weeks 4 days ago