Julia L. Lawall and Harry G. Mairson
Sharing continuations: proofnets for
languages with explicit control
In Programming Languages & Systems, 9th European Symp. Programming, volume 1782 of LNCS, pages 245-259 Springer-Verlag, 2000
We introduce graph reduction technology that
implements functional languages with control, such
as Scheme with call/cc, where continuations
can be manipulated explicitly as values, and can be
optimally reduced in the sense of Lévy. The
technology is founded on proofnets for
multiplicative-exponential linear logic, extending
the techniques originally proposed by Lamping, where
we adapt the continuation-passing style
transformation to yield a new understanding of
sharable values. Confluence is maintained by
returning multiple answers to a (shared)
continuation. Proofnets provide a
concurrent version of linear logic proofs,
eliminating structurally irrelevant
sequentialization, and ignoring asymmetric
distinctions between inputs and outputs-dually,
expressions and continuations. While Lamping's
graphs and their variants encode an embedding of
intuitionistic logic into linear logic, our
construction implicitly contains an embedding of
classical logic into linear logic.
We propose a
family of translations, produced uniformly by
beginning with a continuation-passing style
semantics for the languages, employing standard
codings into proofnets using call-by-value,
call-by-name-or hybrids of the two-to locate
proofnet boxes, and converting the proofnets
to direct style. The resulting graphs can be reduced
simply (cut elimination for linear logic), have a
consistent semantics that is preserved by reduction
(geometry of interaction, via the so-called
context semantics), and allow shared, incremental
evaluation of continuations (optimal reduction).
[ bib |
.ps.gz |
.pdf.gz |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
