Lambda the Ultimate

Buffer overflows are one problem that the world seems to know how to solve, as evidenced by languages such as Java, C#, and Python that are not susceptible to the issue. On the surface, the reason why we still are plagued by the problem is obvious: we still use C, C++, and assembly in a heck of a lot of applications.

Among the things mentioned in this essay: String-handling libraries, Static analysis tools, Cyclone, and zero knowledge protocols.

What happened to all the editors? Is everyone on vaction? ;-)

... or how is the title of this paper pronounced?

We make the notion of scope in the lambda-calculus explicit. To that end, the syntax of the lambda-calculus is extended with an end-of-scope operator [adbmal], matching the usual opening of a scope due to lambda. Accordingly, beta-reduction is extended to the set of scoped lambda-terms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped beta-reduction. Confluence of beta-reduction for the ordinary lambda-calculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, alpha-equivalence is needed. All our proofs have been verified in Coq.

While playing with my own lambda-machine (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.