Ocsigen [1] est une plateforme pour développer et déployer des sites Web dynamiques. Elle est basée sur la définition de services, implémentés par des fonctions Caml dont l'exécution est déclenchée par une requête HTTP, et qui génèrent la réponse du serveur. Ces services peuvent être créés dynamiquement en réponse à des actions de l'utilisateur, et concerner tous les utilisateurs ou seulement une session. Plusieurs types de services permettent d'implémenter divers comportements utiles pour des applications Web. Le but de ce stage est de définir des contracts [2,3] c'est à dire des abstractions du comportement observable de services Ocsigen, et de les utiliser pour vérifier la composition, la mise à jour et la coordination de services Ocsigen. L'idée est de pouvoir détecter statiquement des problèmes dans les développement et la mise à jour des applications Ocsigen tels que des boucles d'appels de services ou du code mort, ainsi que de fournir une spécification formelle des services à utiliser non seulement pour leur développement modulaire mais aussi pour leur documentation et pour des recherches dans des bibliothèques.

Rémunération possible

Bonne connaissance de la théorie de la concurrence et des algèbres de processus ainsi que de la théorie des types et de la programmation fonctionnelle.

Giuseppe Castagna and Vincent Balat : Laboratoire PPS, Université Paris 7.