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
3 days 19 hours ago
5 days 14 hours ago
2 weeks 2 days ago
3 weeks 1 day ago
4 weeks 1 day ago
5 weeks 6 days ago
6 weeks 2 days ago
7 weeks 3 days ago
7 weeks 6 days ago
8 weeks 2 hours ago