ReactiveML est un langage dédié à la programmation de systèmes
interactifs tels que des interfaces graphiques, jeux vidéos ou
simulations. Le langage ajoute des constructions de programmation
concurrente coopérative a un langage à la ML
(ici
OCaml).
Le modèle de concurrence est fondé sur
le
modèle réactif synchrone introduit par Frédéric Boussinot.
Elip et Glonemo sont deux simulateurs de réseaux ad hoc programmés en
ReactiveML. Il font chacun environ 1700 lignes de code source. Elip
est un simulateur de protocoles de routage dans les réseaux mobiles ad
hoc réalisé en collaboration avec Farid Benbadis de l'équipe réseaux
du LIP6. Les simulations décrites dans les articles de F. Benbadis,
M. Dias de Amorim et S. Fdida sur le protocole ELIP ont été réalisées
avec ce simulateur.
Glonemo est un simulateur de consommation d'énergie dans les
réseaux de capteurs. Ludovic Samper (France Telecom/Verimag) en
est le développeur principal.
Glouton est une implantation de la
bibliothèque
Junior
de programmation réactive en Java.
On peut trouver dans les thèses de Raúl Acosta-Bermejo et Christian
Brunette des comparaisons de Glouton avec les autres implantations de
Junior. Ces analyses montrent que notre implantation est aussi
efficace que les meilleures et a l'avantage d'être formellement
décrite.
Le n-synchrone est un modèle de programmation qui permet de définir
des réseaux de Kahn à mémoire bornée et de calculer automatiquement la
taille des buffers.
Lucy-n est un langage pour la programmation dans le modèle
n-synchrone. Il est similaire au langage flot de données synchrone
Lustre auquel une construction de buffer a été ajouté.
Nous avons développé un compilateur prototype pour ce langage. La
particularité du compilateur est que le calcul d'horloge est implanté
sous forme de foncteurs. Il est ainsi paramétré par le langage
d'horloges et l'algorithme de résolution des contraintes de
sous-typage. Ceci nous permet d'expérimenter simplement différentes
techniques de résolution.
Par ailleurs, nous fournissons des outils en ligne de commande pour
manipuler les horloges et des abstractions de celles-ci.
Enfin, nous avons prouvé en Coq des propriétés algébriques sur les
mots binaires que sont les horloges et la correction des opérations abstraites sur
ces mots. Ceci correspond à environ 1800 lignes de
spécifications et 7000 lignes de preuves.
L'outil aadl2sync traduit des fichiers de description d'architectures
matérielles et logicielles en AADL vers le langage synchrone flot de
données SCADE. Ce compilateur a été développé dans le cadre du projet
européen ASSERT en collaboration avec Erwan Jahier. Nous distribuons
également
aadl4ocaml,
un parseur de AADL pour OCaml.
JoCaml est une extension d'OCaml pour la programmation de systèmes
concurrents et distribués. Il se fonde sur le join-calcul, un calcul
de processus asynchrone. J'ai participé à la mise au point, à la
réalisation d'applications et à la rédaction de la documentation de la
nouvelle version du langage. Luc Maranget en est le développeur
principal.
X10 est un langage orienté objet. Une de ses particularité est qu'il
dispose d'un système de type très riche dans lequel il est possible
d'exprimer des contraintes. En collaboration avec Vijay Saraswat et
Olivier Tardieu, j'ai ajouté au langage un mécanisme d'inférence de
contraintes.
Q*cert est un compilateur de requêtes écrit dans l'assistant de preuve
Coq. Le compilateur accepte plusieurs langages d'entrée comme SQL et
OQL et peut produire par exemple du code JavaScript, Spark ou
Cloudant. Il repose sur l'algèbre relationnelle imbriquée.
Un langage de script pour analyser des données textuelles semi-structurées.
wcs-ocaml est un environnement de développement en OCaml et un outil en ligne de commande pour Watson Conversation Service (WCS). Il permet de programmer des chat bots en OCaml.