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 archivesActive forum topicsNew forum topics

Recent comments
3 hours 44 min ago
5 hours 3 min ago
5 hours 25 min ago
8 hours 56 min ago
14 hours 48 min ago
14 hours 54 min ago
16 hours 49 min ago
1 day 2 hours ago
1 day 22 hours ago
2 days 7 hours ago