Tag: proof assistant

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.

Jul 29 2013

A Machine-Checked Proof of the Odd Order Theorem

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