Category: News

May 22 2015

The Coq Workshop 2015

The 7th Coq Workshop will be held in Sophia Antipolis, France – June 26, 2015.

Dec 19 2014

First Coq Coding Sprint – June 22-25 2015 Sophia-Antipolis

All scientific information : https://coq.inria.fr/cocorico/CoqCodingSprint/CoqCS1

Accomodation information

Venue

Aug 08 2014

Yves Bertot récompensé par l’ACM Software System Award

Bruno Barras Yves Bertot Christine Paulin-Mohring Hugo Herbelin Jean-Christophe Filliâtre

Le logiciel Coq est une nouvelle fois récompensé par l’Association for Computing Machinery. ACM Software System Award à San Francisco le 21 juin 2014 prix-ACM Sur la photo, Yves Bertot (2ème sur la gauche) est entouré de quatre des huit autres récipiendaires du Software System Award 2013 :

  • Thierry Coquand, Université de Gothenburg;
  • Gérard Huet, Inria Paris – Rocquencourt;
  • Christine Paulin-Mohring, Université Paris Sud/Inria Saclay -Ile-de-France;
  • Bruno Barras, Inria Saclay/École Polytechnique;
  • Jean-Christophe Filliâtre, CNRS/Inria Saclay – Ile-de-France;
  • Hugo Herbelin, Inria Paris – Rocquencourt;
  • Chet Murthy, Google Inc.;
  • Yves Bertot, Inria Sophia Antipolis-Méditerranée ;
  • Pierre Castéran, Université de Bordeaux.

La vidéo de l’évènement (La même sur youtube), la photographie de la remise de prix.

Apr 17 2014

Coq receives the 2013 Software system Award

Coq selected as recipient of the 2013 Software system Award

    Coq is a software tool for the interactive development of formal proofs, which is a key enabling technology for certified software. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. An open source product, Coq has played an influential role in formal methods, programming languages, program verification and formal mathematics. As certification gains importance in academic and industrial arenas, Coq plays a critical role as a primary programming and certification tool. Coq’s first implementation was in 1985, when it was named CoC (the acronym for the logic it implemented: the Calculus of Constructions). This system was developed by the Coq Development Team whose primary members were Thierry Coquand, University of Gothenburg; Gérard Huet, INRIA Paris – Rocquencourt; Christine Paulin-Mohring, University Paris Sud/INRIA Saclay; Bruno Barras, INRIA Saclay/École Polytechnique; Jean-Christophe Filliâtre, CNRS/INRIA Saclay; Hugo Herbelin, INRIA Paris – Rocquencourt; Chet Murthy, Google Inc.; Yves Bertot, INRIA Sophia; and Pierre Castéran, University of Bordeaux.

ACM will present the 2013 Software System Award at its annual Awards Banquet on June 21 in San Francisco, CA.

Nov 26 2013

Vladimir Voevodsky’s interview about Mathematical Revolution

Interview de Vladimir Voevodsky  : http://blogs.scientificamerican.com/guest-blog/2013/10/01/voevodskys-mathematical-revolution/

Jul 30 2013

Démonstration du théorème Feit-Thompson : La précision des ordinateurs au service des mathématiques

Sorry, this entry is only available in French.

Jul 30 2013

Démonstration du théorème Feit-Thompson : Un grand succès pour la preuve informatique

Sorry, this entry is only available in French.

Jul 30 2013

The Coq proof assistant is the recipient of the 2013 software award

http://www.sigplan.org/Awards/Software/Main/

Jul 30 2013

Coq, les maths ont trouvé leur maître (Article de Science et Vie magazine)

Sorry, this entry is only available in French.

Jul 29 2013

A Machine-Checked Proof of the Odd Order Theorem

http://hal.inria.fr/hal-00816699/en/