Source author record

Olivier Danvy

Olivier Danvy appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Programming Languages Logic in Computer Science Software Engineering

Catalog footprint

What is connected

4works

3topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2016arXiv

Proceedings of the Workshop on Continuations

The notion of continuation is ubiquitous in many different areas of computer science, including systems programming, programming languages, algorithmics, semantics, logic, and constructive mathematics. In fact the concept of continuation nicely realizes sophisticated control mechanisms, which are widely used in a variety of applications. Since we cannot escape control features, it becomes a challenge to provide them with sound reasoning principles. Indeed there is much research activity on understanding, representing, and reasoning about elaborated non-local control structures, in particular in declarative programming languages such as functional and logic languages. The proceedings of the Workshop on Continuations 2015, held in London in April 2015, illustrate some of the afore mentioned topics and hopefully they will inspire further research work on the subject.

preprint2013arXiv

Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday

This Liber Amicorum is a collection of essays ranging from personal memories to technical contributions. It is a tribute to Dave Schmidt and his career, and was composed at the occasion of his sixtieth birthday.

preprint2011arXiv

Proceedings IFIP Working Conference on Domain-Specific Languages

This volume is the proceedings of the second IFIP Working Conference on Domain-Specific Languages (DSL 2011). It contains 2 abstracts of invited presentations, 7 peer-reviewed articles selected by the program committee from 14 submissions, and 6 lecture notes for the distilled tutorials that we solicited.

preprint2008arXiv

A Rational Deconstruction of Landin's SECD Machine with the J Operator

Landin's SECD machine was the first abstract machine for applicative expressions, i.e., functional programs. Landin's J operator was the first control operator for functional languages, and was specified by an extension of the SECD machine. We present a family of evaluation functions corresponding to this extension of the SECD machine, using a series of elementary transformations (transformation into continu-ation-passing style (CPS) and defunctionalization, chiefly) and their left inverses (transformation into direct style and refunctionalization). To this end, we modernize the SECD machine into a bisimilar one that operates in lockstep with the original one but that (1) does not use a data stack and (2) uses the caller-save rather than the callee-save convention for environments. We also identify that the dump component of the SECD machine is managed in a callee-save way. The caller-save counterpart of the modernized SECD machine precisely corresponds to Thielecke's double-barrelled continuations and to Felleisen's encoding of J in terms of call/cc. We then variously characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. As a byproduct, we also present several reduction semantics for applicative expressions with the J operator, based on Curien's original calculus of explicit substitutions. These reduction semantics mechanically correspond to the modernized versions of the SECD machine and to the best of our knowledge, they provide the first syntactic theories of applicative expressions with the J operator.