PPS, Université Paris 7
PPS is a leading research laboratory that federates mathematicians and computer scientists to work on programming languages, distributed systems, and their logical foundations. It has a internationally recognized expertize in XML programming languages having developed or co- developed reference languages such as XDuce and CDuce, in particular for what concerns XML type systems. The group actively contributes to the theoretical research around the formalism that underlies the Coq proof assistant, as well as to the development of/in Coq of which it is one of the main current contributors.
LRI, Université Paris-Sud
The LRI partner gathers the data-centric languages and the proof of programs groups of ProVal, a project-team of the INRIA Saclay - Île-de-France research center, joint with LRI (CNRS and University of Paris Sud), located in Orsay, France . The former group has a long and recog- nized experience in developing frameworks adapted to reason about and efficiently implement query languages. It actively contributed, and still does, in the design, maintenance and further extensions of CDuce. The latter group is a world-wide recognized leader in the design, imple- mentation and maintenance of the Coq proof assistant. The objective of the team is to propose methods and tools that can be integrated into the software development cycle and that make it possible to produce code that is proven to be correct with respect to its expected behavior. The team develops a generic program proof environment (the Why platform), that is able to gener- ate proof demands that can then be delegated to automatic (eg., Alt-ergo) or interactive provers. Dedicated environments to prove C programs (Caduceus) and Java programs (Krakatoa) annoted with formulas describing the expected behavior, are constructed on top of this tool.
WAM EPI
WAM is a project-team of the INRIA Grenoble - Rhône-Alpes research center, joint with LIG (CNRS and University of Grenoble), located in Montbonnot, France. This group has a long and recognized experience in developing XML Document process- ing systems, automatic content adaptation by transformation and multimedia mobile document systems. The group actively contributes to the design and implementation of XML/XPath static analyzers with logical solvers, XML document processing tool-chains and document standards. The group is involved in the World Wide Web Consortium activities since 1995. Vincent Quint, the group leader, is member of the W3C Advisory Committee and former deputy director for Eu- rope of the W3C. Nabil Layaïda is also a member of the W3C Synchronized Multimedia working group.