Sites Inria

Version française


A technology development action for Coq

The Coq technology development action involves a collection of people and teams working together to roll out Coq proof assistant software.

This software is used internationally by the academic world in fields such as teaching, program language specification and mathematical formalisation. The demonstration of the four-colour theorem with Coq is one famous example. It is a key tool for companies such as Gemalto and Trusted Logic, which need to guarantee high levels of security for purposes such as online credit card payments.

 Software maintenance is mainly the preserve of Inria researchers spread among three centres in Paris-Rocquencourt (PI.R2), Saclay (Typical, Proval) and Sophia Antipolis (Marelle). "Being based at several sites makes interaction more difficult, and this is what prompted us to request a technology development action," explains Hugo Herbelin, coordinator of the Coq technology development action. "It provides us with additional resources and two engineers to work on the graphical interface and the interface with other tools. This allows us to make our multi-site development official and provides a certain continuity."

Keywords: Coq Software Paris - Rocquencourt