Fabien DAGNAT

Fabien DAGNAT


Enseignant-chercheur

Dépt. Informatique

Téléphone : 02 29 00 14 09
Télécopie : 02 29 00 12 82
Courriel : fabien.dagnat@telecom-bretagne.eu
TELECOM Bretagne
Vue aérienne

ReCaml

If you are commited to the domain of dynamic updates or reconfiguration, I invite you to submit a paper to HotSWUp http://www.hotswup.org/2011/...


The paper has been accepted to ICFP 2010, it will be presented in Baltimore at the end of September.

This page supports a paper that, with Jérémy Buisson, we have submitted to ICFP2010. The paper is about our ReCaml proposal.

Abstract

  Most current techniques fail to achieve the dynamic update of recursive functions. A focus on execution states appears to be  essential in order to implement dynamic update in this case. It  indeed alleviates restrictions on the active status of updated elements. We therefore propose a novel language construct for the introspection of execution states, which matches a delimited continuation with a pattern. With formal semantics and type system, (1) unsound update programs can be detected statically and (2) the implementation does not need any specific compilation scheme. This represents one step towards formally verifiable dynamic updates and improved applicability. Beyond the simple example presented in this article, our approach can be applied to dynamically update schedulers, interrupt handlers, reactive systems and interaction loops.

Categories and Subject Descriptors D.3.2 [Programming Languages]: Language Classifications—Applicative (functional) languages; D.3.3 [Programming Languages]: Language Constructs and Features—Control structures;    D.3.4 [Programming Languages]:Processors—Compilers; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages
General Terms Languages
Keywords dynamic software updating, continuation, functional language, execution state introspection, static typing, Caml

The paper submitted

The first resource provided on this page is the paper itself.


Provided additionnal material

This site provides also complementary material to support the paper:

  1. The code of the proof made in coq.
  2. The Caml code of the prototype implementation of ReCaml.
  3. The ReCaml code of the example described in the paper.
Technopôle Brest-Iroise - CS 83818 - 29238 Brest Cedex 3 - France
Tél : 33 (0)2 29 00 11 11 - Fax : 33 (0)2 29 00 10 00