Nicolas Magaud

J. Autom. Reason., March, 2024

Towards Automatic Transformations of Coq Proof Scripts.

[BibT_eX]

[DOI]

Marie-Andrée Jacob-Da Col

CoRR, 2024

2022

Some representations of real numbers using integer sequences.

[BibT_eX]

[DOI]

Loïc Mazo

Laurent Fuchs

Gaëlle Skapin

Math. Struct. Comput. Sci., May, 2022

Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families.

[BibT_eX]

[DOI]

Catherine Dubois

Alain Giorgetti

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

Spreads and Packings of PG(3, 2), Formally!

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Automated Deduction in Geometry, 2021

Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Automated Deduction in Geometry, 2021

Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

Two New Ways to Formally Prove Dandelin-Gallucci's Theorem.

[BibT_eX]

[DOI]

Proceedings of the ISSAC '21: International Symposium on Symbolic and Algebraic Computation, 2021

2020

Contributions au développement des méthodes formelles de preuves et applications à la géométrie.

[BibT_eX]

[DOI]

, 2020

2019

Two cryptomorphic formalizations of projective incidence geometry.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2019

2018

Formalizing Some "Small" Finite Models of Projective Geometry in Coq.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 2018

2015

Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective.

[BibT_eX]

[DOI]

Agathe Chollet

Laurent Fuchs

Ann. Math. Artif. Intell., 2015

2012

A case study in formalizing projective geometry in Coq: Desargues theorem.

[BibT_eX]

[DOI]

Julien Narboux

Comput. Geom., 2012

Designing and proving correct a convex hull algorithm with hypermaps in Coq.

[BibT_eX]

[DOI]

Christophe Brun

Jean-François Dufourd

Comput. Geom., 2012

Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls.

[BibT_eX]

[DOI]

Christophe Brun

Jean-François Dufourd

Proceedings of the Automated Deduction in Geometry - 9th International Workshop, 2012

2009

Formalizing Desargues' theorem in Coq using ranks.

[BibT_eX]

[DOI]

Julien Narboux

Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), 2009

2008

Formalizing Projective Plane Geometry in Coq.

[BibT_eX]

[DOI]

Julien Narboux

Proceedings of the Automated Deduction in Geometry - 7th International Workshop, 2008

2003

Changements de Représentation des Données dans le Calcul des Constructions. (Changing Data Representation in the Calculus of Constructions).

[BibT_eX]

[DOI]

PhD thesis, 2003

Changing Data Representation within the Coq System.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2002

A Proof of GMP Square Root.

[BibT_eX]

[DOI]

Yves Bertot

Paul Zimmermann

J. Autom. Reason., 2002

2001

Changement de représentation des structures de données en Coq: le cas des entiers naturels.

[BibT_eX]

Yves Bertot

Proceedings of the Journées francophones des langages applicatifs (JFLA'01), 2001

2000

Changing Data Structures in Type Theory: A Study of Natural Numbers.

[BibT_eX]

[DOI]