Tag: Coq

Jan 29 2015

Marelle Seminar: Proofs as documents: asynchronous interaction for Coq

On Thursday 29/01/2015, at 10h30, in room Byron Blanc,

Speaker: Carst Tankink

Title: Proofs as documents: asynchronous interaction for Coq

Abstract:Since the beginning of interactive theorem proving, the actual interaction has been a simple back-and-forth between the user and the prover, with the user providing a command the prover eagerly executes, giving feedback the user then uses to compose a new command. I will present a document-oriented model for Coq proofs (based on Wenzel’s PIDE architectures for Isabelle) that asynchronously updates the proof and processes the results from the prover. This model allows faster (parallel) processing of complete proof scripts, supports a simpler interaction model for readers of formal proofs, and gives a cleaner API for writing third party tools working on top of the proof assistant’s results. I will demonstrate the model and the interactions it allows using the jEdit plugin for Coq.

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.

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/

Nov 22 2013

Séminaire Marelle : A Coq formalization of finitely presented modules.

On Friday 22/11/2013, at 10h30, in room Byron Beige,

Speaker: Cyril Cohen.
Joint work with: Anders Mortberg.

Title: A Coq formalization of finitely presented modules.

Abstract:
The use of vector spaces in homology theory does not give as precise
information as with modules. A generalization to finitely presented modules
covers computable Z-homology, which gives finer-grained topological invariants.
We formalize a construction of finitely presented modules over coherent and
strongly discrete rings and discuss its properties. This formalization gives
basic building blocks that lead to a clean definition of homology groups.

Nov 20 2013

Soutenance de Thèse : Étude formelle d’algorithmes efficaces en algèbre linéaire

Sorry, this entry is only available in French.

Aug 26 2013

Séminaire Marelle : Certified, Efficient and Sharp Univariate Taylor Models in COQ.

On Monday 26/08/2013, at 14h30, in room Byron Blanc.

Speaker: Érik Martin-Dorel.

Title: Certified, Efficient and Sharp Univariate Taylor Models in COQ.

Abstract:
We present a formalisation, within the COQ proof assistant, of
univariate Taylor models. This formalisation being executable, we get a
generic library whose correctness has been formally proved and with
which one can effectively compute rigorous and sharp approximations of
univariate functions composed of usual functions such as 1/x, sqrt(x),
exp(x), sin(x) among others. In this talk, we present the key parts of
the formalisation and we evaluate the quality of our certified library
on a set of examples.

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.