Publications de l'équipe MARELLE

2012

Communications avec actes

Titre

Rigorous Polynomial Approximation using Taylor Models in Coq

Auteurs

Nicolas Brisebarre; Mioara Joldes; Érik Martin-Dorel; Micaela Mayero; Jean-Michel Muller ; Ioana Pasca; Laurence Rideau; Laurent Théry

Détail

Alwyn Goodloe and Suzette Person. Fourth NASA Formal Methods Symposium, Apr 2012, Norfolk, Virginia, United States. Springer, pp. 15, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Towards a certified computation of homology groups for digital images

Auteurs

Jónathan Heras; Maxime Dénès ; Gadea Mata; Anders Mortberg; María Poza; Vincent Siles

Détail

CTIC - Computational Topology in Image Context - 2012, May 2012, Bertinoro, Italy. Springer, Computational Topology in Image Context, 7309, pp. 49-57, Lecture Notes In Computer Science

Accès au texte intégral et bibtex

Titre

A refinement-based approach to computational algebra in COQ

Auteurs

Maxime Dénès ; Anders Mortberg; Vincent Siles

Détail

Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, Interactive Theorem Proving, 7406, pp. 83-98, Lecture Notes In Computer Science

Accès au texte intégral et bibtex

2011

Articles dans des revues avec comité de lecture

Titre

Incidence simplicial matrices formalized in Coq/SSReflect

Auteurs

Jónathan Heras; María Poza; Maxime Denes; Laurence Rideau

Détail

Lecture Notes in Artificial Intelligence, Springer, 2011

Accès au texte intégral et bibtex

Titre

Full reduction at full throttle

Auteurs

Mathieu Boespflug ; Maxime Dénès ; Benjamin Grégoire

Détail

Lecture notes in computer science, Springer, 2011, Certified Programs and Proofs

Accès au texte intégral et bibtex

Titre

A formal study of Bernstein coefficients and polynomials

Auteurs

Yves Bertot; Frédérique Guilhot; Assia Mahboubi

Détail

Mathematical Structures in Computer Science, Cambridge University Press, 2011, 21 (04), pp. 731-761

Accès au texte intégral et bibtex

Communications avec actes

Titre

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Auteurs

Michaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Thery; Benjamin Werner

Détail

Jouannaud, Jean-Pierre and Shao, Zhong. CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan, Province Of China. Springer, Certified Programs and Proofs, 7086, pp. 135-150, Lecture notes in computer science - LNCS

Accès au texte intégral et bibtex

Titre

A Formalization of Polytime Functions

Auteurs

Sylvain Heraud; David Nowak

Détail

ITP 2011, Aug 2011, Nijmegen, Netherlands.

Accès au texte intégral et bibtex

Titre

A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry

Auteurs

Laurent Fuchs; Laurent Thery

Détail

Pascal Schreck, Julien Narboux and Jürgen Richter-Gebert. Automated Deduction in Geometry, ADG 2010, Jul 2010, Munich, Germany. Springer, 6877, pp. 51-62, 2011, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry

Auteurs

Tuan Minh Pham; Yves Bertot; Julien Narboux

Détail

The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Jun 2011, Santander, Spain. Springer-Verlag, 6785, pp. 368-383, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Verifying SAT and SMT in Coq for a fully automated decision procedure

Auteurs

Mickaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Théry; Benjamin Wener

Détail

PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland.

Accès au texte intégral et bibtex

Communications sans actes

Titre

A Flexible Proof Format for SMT: a Proposal

Auteurs

Frédéric Besson; Pascal Fontaine ; Laurent Théry

Détail

Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland.

Accès au texte intégral et bibtex

Rapports

Titre

Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers

Auteurs

José Grimm

Détail

[Research Report], 2011, pp. 446. RR-7150

Accès au texte intégral et bibtex

Thèses

Titre

Terminaison basée sur les types et filtrage dépendant pour le calcul des constructions inductives

Auteurs

Jorge Sacchini

Détail

Informatique temps réel, robotique et automatique. École Nationale Supérieure des Mines de Paris, Jun. 2011. English

Accès au texte intégral et bibtex

2010

Articles dans des revues avec comité de lecture

Titre

Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs

Auteurs

Tuan Minh Pham

Détail

SAC '10 Proceedings of the 2010 ACM Symposium on Applied Computing, ACM Proceeding, 2010

Accès au texte intégral et bibtex

Titre

Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving

Auteurs

Benjamin Grégoire; Loïc Pottier; Laurent Théry

Détail

LNAI, Springer Verlag, 2010, Post-proceedings of ADG 2008 (Automated Deduction in Geometry)

Accès au texte intégral et bibtex

Communications avec actes

Titre

On Strong Normalization of the Calculus of Constructions with Type-Based Termination

Auteurs

Benjamin Grégoire; Jorge Sacchini

Détail

Christian G. Fermüller and Andrei Voronkov. 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Oct 2010, Yogyakarta, Indonesia. Springer, 6397, pp. 333-347, Lecture notes in computer science

Accès au texte intégral et bibtex

Titre

Formal study of plane Delaunay triangulation

Auteurs

Jean-François Dufourd; Yves Bertot

Détail

Paulson, Lawrence and Kaufmann, Matt. Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, Interactive Theorem Proving, 6172, pp. 211-226, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Formally Verified Conditions for Regularity of Interval Matrices

Auteurs

Ioana Pasca

Détail

Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, Intelligent Computer Mathematics, 6167, pp. 219-233, LNAI

Accès au texte intégral et bibtex

Titre

Extending Coq with Imperative Features and its Application to SAT Verification

Auteurs

Michaël Armand; Benjamin Grégoire; Arnaud Spiwack; Laurent Théry

Détail

Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Titre

A Machine-Checked Formalization of Sigma-Protocols

Auteurs

Gilles Barthe; Daniel Hedin; Santiago Zanella Beguelin; Benjamin Gregoire; Sylvain Heraud

Détail

CSF'10, Jul 2010, Edinburgh, Sweden. IEEE, 23rd IEEE Computer Security Foundations Symposium CSF 2010, pp. 246-260

Accès au texte intégral et bibtex

Titre

Programming Language Techniques for Cryptographic Proofs

Auteurs

Gilles Barthe; Benjamin Gregoire; Santiago Zanella Beguelin

Détail

Matt Kaufmann and Lawrence C. Paulson. ITP'10, 2010, Edinburgh, United Kingdom. Springer, Interactive Theorem Proving, 6172, pp. 115-130, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Conférences invitées

Titre

A combination of a dynamic geometry software with a proof assistant for interactive formal proofs

Auteurs

Tuan Minh Pham; Yves Bertot

Détail

9th International Workshop On User Interfaces for Theorem Provers FLOC'10 Satellite Workshop, Jul 2010, Edinburgh, Scotland, United Kingdom. Elsevier, Proceedings 9th International Workshop On User Interfaces for Theorem Provers, Electronic Notes in Theoretical Computer Science (ENTCS)

Accès au texte intégral et bibtex

Cours

Titre

Coq in a Hurry

Auteurs

Yves Bertot

Détail

3eme cycle. Types Summer School, also used at the University of Goteborg, Nice,
Ecole Jeunes Chercheurs en Programmation,
Universite de Nice, pp. 43, May. 2010

Accès au texte intégral et bibtex

Rapports

Titre

Formal Proofs for Theoretical Properties of Newton's Method

Auteurs

Ioana Pasca

Détail

[Research Report], 2010. RR-7228

Accès au texte intégral et bibtex

Thèses

Titre

Certification formelle de preuves cryptographiques basées sur les séquences de jeux

Auteurs

Santiago Zanella Beguelin

Détail

Informatique temps réel, robotique et automatique. École Nationale Supérieure des Mines de Paris, Dec. 2010. English

Accès au texte intégral et bibtex

Titre

Vérification formelle pour les méthodes numériques

Auteurs

Ioana Pasca

Détail

Université de Nice Sophia-Antipolis, Nov. 2010. English

Accès au texte intégral et bibtex

Titre

Composants mathématiques pour la théorie des groupes

Auteurs

Sidi Ould Biha

Détail

informatique. Université de Nice Sophia-Antipolis, Feb. 2010. French

Accès au texte intégral et bibtex

2009

Communications avec actes

Titre

Packaging Mathematical Structures

Auteurs

François Garillot; Georges Gonthier; Assia Mahboubi; Laurence Rideau

Détail

Tobias Nipkow and Christian Urban. Theorem Proving in Higher Order Logics, 2009, Munich, Germany. Springer, 5674, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Formal verification of exact computations using Newton's method

Auteurs

Nicolas Julien; Ioana Pasca

Détail

Theorem Proving in Higher Order Logics, Aug 2009, Munich, Germany. Springer, Theorem Proving in Higher Order Logics, 5674, pp. 408-423, LNCS

Accès au texte intégral et bibtex

Titre

Finite groups representation theory with Coq

Auteurs

Sidi Ould Biha

Détail

8th International Conference on Mathematical Knowledge Management, Jul 2009, Grand Bend, Ontario, Canada.

Accès au texte intégral et bibtex

Titre

Formal proof of theorems on genetic regulatory networks

Auteurs

Maxime Dénès; Benjamin Lesage; Yves Bertot; Adrien Richard

Détail

SYNASC'09, Sep 2009, Timisoara, Romania. IEEE, Synasc 2009, 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing

Accès au bibtex

Titre

A New Elimination Rule for the Calculus of Inductive Constructions

Auteurs

Bruno Barras; Pierre Corbineau; Benjamin Grégoire; Hugo Herbelin; Jorge Sacchini

Détail

Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro. Types for Proofs and Programs, Mar 2008, Torino, Italy. Springer, Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, 5497, pp. 32-48, 2009, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Rapports

Titre

Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets

Auteurs

José Grimm

Détail

[Research Report], 2009, pp. 225. RR-6999

Accès au texte intégral et bibtex

2008

Articles dans des revues avec comité de lecture

Titre

Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves

Auteurs

Laurence Rideau; Bernard Serpette; Xavier Leroy

Détail

Journal of Automated Reasoning, Springer, 2008, 40 (4), pp. 307-326

Accès au texte intégral et bibtex

Communications avec actes

Titre

Fixed point semantics and partial recursion in Coq

Auteurs

Yves Bertot; Vladimir Komendantsky

Détail

PPDP 2008, Jul 2008, Valencia, Spain.

Accès au texte intégral et bibtex

Titre

Certified exact real arithmetic using co-induction in arbitrary integer base

Auteurs

Nicolas Julien

Détail

FLOPS 2008, Apr 2008, ISE, Japan.

Accès au texte intégral et bibtex

Titre

Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton

Auteurs

Sidi Ould Biha

Détail

JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp. 1-14

Accès au texte intégral et bibtex

Titre

A Formal Verification for Kantorovitch's Theorem

Auteurs

Ioana Pasca

Détail

JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp. 15-30

Accès au texte intégral et bibtex

Titre

Inductive and Coinductive Components of Corecursive Functions in Coq

Auteurs

Yves Bertot; Ekaterina Komendantskaya

Détail

Jiri Adamek. Coalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary.

Accès au texte intégral et bibtex

Titre

Fibrational semantics for many-valued logic programs: grounds for non-groundness.

Auteurs

Ekaterina Komendantskaya; John Power

Détail

JELIA, Aug 2008, Dresden, Germany.

Accès au texte intégral et bibtex

Titre

Using Structural Recursion for Corecursion

Auteurs

Yves Bertot; Ekaterina Komendantskaya

Détail

Stefano Berardi and Feruccio Damiani and Ugo de Liguoro. Types 2008, 2008, Torino, Italy. Springer, 5497, pp. 220-236, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Structural abstract interpretation, A formal study using Coq

Auteurs

Yves Bertot

Détail

Ana Bove and Jorge Sousa Pinto. LERNET Summer School, Feb 2008, Piriapolis, Uruguay. Springer, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Canonical Big Operators

Auteurs

Yves Bertot; Georges Gonthier; Sidi Ould Biha; Ioana Pasca

Détail

Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. 5170/2008, LNCS

Accès au texte intégral et bibtex

Titre

Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics

Auteurs

Loïc Pottier

Détail

Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and Konev, B. and Schulz, S.. Knowledge Exchange: Automated Provers and Proof Assistants, Nov 2008, Doha, Qatar. pp. 418, CEUR Workshop Proceedings

Accès au texte intégral et bibtex

2007

Communications avec actes

Titre

Primality Proving with Elliptic Curves

Auteurs

Laurent Théry; Guillaume Hanrot

Détail

Klaus Schneider and Jens Brandt. TPHOL 2007, Sep 2007, Kaiserslautern, Germany. Springer-Verlag, Theorem Proving in Higher Order Logics, 4732, pp. 319-333, LNCS

Accès au texte intégral et bibtex

Rapports

Titre

Proving the group law for elliptic curves formally

Auteurs

Laurent Thery

Détail

[Technical Report], 2007, pp. 16. RT-0330

Accès au texte intégral et bibtex

Titre

A Modular Formalisation of Finite Group Theory

Auteurs

Georges Gonthier; Assia Mahboubi; Laurence Rideau; Enrico Tassi; Laurent Théry

Détail

[Research Report], 2007, pp. 17. RR-6156

Accès au texte intégral et bibtex

Titre

Theorem proving support in programming language semantics

Auteurs

Yves Bertot

Détail

[Research Report], 2007, pp. 23. RR-6242

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves

Auteurs

Laurence Rideau; Bernard Serpette; Xavier Leroy

Détail

Oct. 2007

Accès au texte intégral et bibtex

2006

Articles dans des revues avec comité de lecture

Titre

Affine functions and series with co-inductive real numbers

Auteurs

Yves Bertot

Détail

Mathematical Structures in Computer Science, Cambridge University Press, 2006, 17 (1), pp. 37-63

Accès au texte intégral et bibtex

Communications avec actes

Titre

Proving formally the implementation of an efficient gcd algorithm for polynomials

Auteurs

Assia Mahboubi

Détail

Ulrich Furbach and Natarajan Shankar. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Aug 2006, Seattle, WA, United States. Springer, 4130, pp. 438-452, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

A structured approach to proving compiler optimizations based on dataflow analysis

Auteurs

Yves Bertot; Benjamin Grégoire; Xavier Leroy

Détail

Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. Springer, Types for Proofs and Programs International Workshop, TYPES 2004, Revised Selected Papers, 3839, pp. 66-81, 2006, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Conférences invitées

Titre

Arithmétique réelle exacte certifiée, co-induction et base arbitraire

Auteurs

Nicolas Julien

Détail

Journées Francophones des Langages Applicatifs, Jan 2007, Aix-les-Bains.

Accès au texte intégral et bibtex

Cours

Titre

lambda-calcul et types

Auteurs

Yves Bertot

Détail

Ecole Jeunes Chercheurs en Programmation (CNRS-INRIA) Toulouse, 2006

Accès au texte intégral et bibtex

Rapports

Titre

Extending the Calculus of Constructions with Tarski's fix-point theorem

Auteurs

Yves Bertot

Détail

[Research Report], 2006, pp. 15

Accès au texte intégral et bibtex

Titre

Formalising Sylow's theorems in Coq

Auteurs

Laurent Thery; Laurence Rideau

Détail

[Technical Report], 2006, pp. 23. RT-0327

Accès au texte intégral et bibtex

Titre

Ambiguous Typing

Auteurs

Loïc Pottier

Détail

[Research Report], 2006, pp. 11. RR-6041

Accès au texte intégral et bibtex

Thèses

Titre

Contributions à la certification des calculs dans R : théorie, preuves, programmation

Auteurs

Assia Mahboubi

Détail

informatique. Université de Nice Sophia-Antipolis, Nov. 2006. French

Accès au texte intégral et bibtex

2005

Articles dans des revues avec comité de lecture

Titre

Vérification formelle d'extractions de racines entières

Auteurs

Yves Bertot

Détail

Revue Technique et Science Informatiques (TSI), Hermes, 2005, Langages Applicatifs, Spécifications, Programmation, Vérification, 24 (9), pp. 1161-1195

Accès au texte intégral et bibtex

Communications avec actes

Titre

Coq à la conquête des moulins

Auteurs

Laurence Rideau; Bernard Serpette

Détail

Olivier Michel. JFLA '2005, Mar 2005, Obernai. INRIA, JFLA 2005 : actes de la conférence journées francophones des langages applicatifs, pp. 169-180

Accès au texte intégral et bibtex

Cours

Titre

CoInduction in Coq

Auteurs

Yves Bertot

Détail

DEA. EU's coordination action Types Goteborg, 2005

Accès au texte intégral et bibtex

2004

Ouvrages scientifiques

Titre

Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions.

Auteurs

Pierre Castéran; Yves Bertot

Détail

Springer Verlag, pp. 470, 2004, Texts in Theoretical Computer Science

Accès au bibtex