ReactiveML compiler (

ReactiveML is a language dedicated to the programming of interactive systems such as video games or discrete simulations. The language add new cooperative concurrent programming constructs to a language à la ML (here OCaml). The concurrency model is based of the synchronous reactive model introduced by Frédéric Boussinot.

ELIP and Glonemo network simulators (

Elip and Glonemo are two ad hoc network simulators programmed in ReactiveML. Elip is a simulator of routing protocols in mobile ad hoc networks. It has been done in collaboration with Farid Benbadis of the Network team of LIP6. It has been used to do the simulations described in the articles of F. Benbadis, M. Dias de Amorim et S. Fdida on the ELIP protocol. Glonemo is a simulator of power consumption in sensor networks. Ludovic Samper (France Telecom/Verimag) is the main developer.

The Glouton library (

Glouton is the implementation of the Junior library for the reactive programming in Java. Comparisons between Glouton and other implementations of Junor can be found in the PhD thesis of Raúl Acosta-Bermejo and Christian Brunette. These analysis show that our implementation is as efficient as the others but has the advantage to be formally specified.

Language, tools and proofs on n-synchrony (

The n-synchronous programming model allows to define Kahn networks with bounded memory and automatically compute the buffer sizes. Lucy-n is a programming language based on this model of computation. It is similar to the synchronous data flow language Lustre with a new buffer construct. In this language, clocks (production and consumption rates) are expressed with ultimately periodic binary words. We have developed a prototype compiler for this language. Moreover, we provides command line tools to manipulate clocks. Finally, we have proved in the Coq proof assistant algebraic properties on ultimately periodic binary words and their abstract representation that is used in the compiler. It corresponds to about 1800 lines of specification and 7000 lines of proofs.

Compilation of AADL to Scade (

The aadl2sync tool translate AADL files describing hardware and software architectures into a model written in synchronous data flow language SCADE. This compiler has been implemented inside the ASSERT European project in collaboration with Erwan Jahier. We also distribute the tool aadl4ocaml, a AADL parser for OCaml.

The JoCaml compiler (

JoCaml is an extension of OCaml for the programming of concurrent and distributed systems. It is based on the join-calculus, an asynchronous process calculus. I have participated to the release of the language. Luc Maranget is the main developer.

The X10 compiler (

X10 is an object-oriented programming language. One of its feature is the type system. It allows to express constraints. In collaboration with Vijay Saraswat and Olivier Tardieu, I have added to the language a way to infer constraints.

The Q*cert compiler (

Q*cert is a query compiler written with the Coq proof assistant. The compiler accept several input languages like SQL and OQL and can produce for example some JavaScript, Spark and Cloudant code. It relies on the Nested Relational Algebra.

The CloudLens scripting language (

A scripting language to analyze semi-structured textual data.

The wcs-ocaml library (

wcs-ocaml is a source development kit in OCaml and command line interface for Watson Conversation Service (WCS). It allows to program chat bots in OCaml.