Lambdascope:

Another optimal implementation of the lambda-calculus

We have presented an implementation of the lambda-calculus

in the spirit of the calculational approach [...], and which

is fully in the traditions of calculi with explicit substitution

and of graph implementations of term rewriting. As far as

we know it is the first such calculus which is optimal in the sense of Levy. Moreover, as far as we know this is the

first optimal calculus featuring only a single scope delimiter

node instead of the usual two, croissants and brackets,

which by force eliminates the problems which are caused by

having more than one scope node [...]. The calculus

is simple, half a page suffices [...] to describe

it, and completely reduction-based (no semantic read-back

in the implementation). As a consequence it can be trivially

implemented in any (modern) programming language.

Remembering our discussion on atoms of PLs (such as scope and name), I decided this paper might be of interest.

## Recent comments

13 weeks 12 hours ago

13 weeks 15 hours ago

13 weeks 16 hours ago

35 weeks 1 day ago

39 weeks 3 days ago

41 weeks 23 hours ago

41 weeks 23 hours ago

43 weeks 5 days ago

48 weeks 3 days ago

48 weeks 3 days ago