Sites Inria

There are 2 Results with the keyword : "Coq"

from left to right : Vinton Cerf, Brent Hailpern, Yves Bertot, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, John White (ACM Chief Executive Officer). - @ACM

ACM award

Software System Award for Coq software


Yves Bertot, leader of Inria's Marelle project team, was invited to San Francisco on 21 June 2013, along with Bruno Barras, Pierre Castéran, Thierry Coquand, Jean-Christophe Filliâtre, Hugo Herbelin, Gérard P. Huet, Chetan Murthy and Christine Paulin-Mohring, to receive the prestigious Software System Award 2013, one of the highest distinctions awarded by AMC, the Association for Computing Machinery. The award, given on the same day as the Turing Award, was for the development of Coq, a proof management system, originally known as COC, the acronym for Calculus of Inductive Constructions. It was the first time in 40 years that the award had gone to a French team, what's more, to a team that also received the ACM SIGPLAN Programming Languages Software Award at the POPL 2014 conference.


Home > Centre > Sophia > News > Software System Award pour le logiciel Coq


© Photo Bernard Lachaud

Computer-Assisted Proof

Using the precision of computers to aid mathematics

Nathaly Mermet, Technoscope - 6/12/2012

Along with the Typical  research team from Inria Saclay – Ile-de-France, the Marelle  research team from the Inria Sophia Antipolis – Mediterranée research centre has made a major contribution to the Mathematical Components project, led by Georges Gonthier as part of the joint Inria – Microsoft Research laboratory. We take a look back at this exciting experience with Marelle researcher Laurence Rideau


Home > Centre > Saclay > News > La précision des ordinateurs au service des mathématiques