Ocsigen [1] is a framework for developping and deploying dynamic Web sites. It is based on the definition of services, implemented by some Caml functions whose execution is generated by HTTP requests that trigger the server answer. These services can by dynamically created as a rection to some user action, and concern all users or just a session. Several kind of services allow the web programmer to implement several features usefule for Web applications. The goal of this project is to devise contracts [2,3], that is, abstractions of the observable behaviour of Ocsigen services and to use them to verify the composition, upgrade, and coordination of Ocsigen services. The goal is to statically detect probems during the development and the upgrade of Ocsigen applications, such as loops of service calls, data races, or dead code. Also, they must provide a formal specification of the services that can be handy not only to the modular development of Web applications, but also to document and automatically search and retrive existing services on the web.

Strong background in concurrency theory and acquaintance with type theory and functional programming programming.

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