[1] David Braun and Nicolas Magaud. Des preuves formelles en Coq du théorème de Thalès pour les cercles. In David Baelde and Jade Alglave, editors, Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA2015), Jan. 2015. Proof development available at http://ddbraun.free.fr. [ bib | http ]
Le théorème de Thalès pour les cercles et sa réciproque qui est plus connue sous le nom de théorème du cercle circonscrit à un triangle rectangle sont des propriétés de géométrie élémentaire enseignées dans les collèges français. Nous nous intéressons non seulement à différentes descriptions possibles de ces propriétés en Coq mais aussi aux preuves correspondantes. Nous étudions notamment comment le choix d'une représentation des objets géométriques contenus dans l'énoncé influencent les arguments de preuve. Nous présentons plusieurs approches, une basée sur des calculs d'angles, une autre basée sur la géométrie analytique et finalement deux démonstrations différentes dans l'axiomatique de Tarski en utilisant dans un cas le théorème de la droite des milieux et dans l'autre la notion de symétrie centrale et ses propriétés.

[2] Nicolas Magaud, Agathe Chollet, and Laurent Fuchs. Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective. Annals of Mathematics and Artificial Intelligence, pages 1--24, 2014. Online First. To appear. Proof development available at https://dpt-info.u-strasbg.fr/~magaud/Harthong-Reeb/. [ bib | http ]
This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb, the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field. The formalization is based on previous work by Chollet, Fuchs et al. where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges. Laugwitz-Schmieden numbers are then introduced and their limitations with respect to being a model of the Harthong-Reeb line is investigated. In this paper, we transpose all these definitions and properties into a formal description using the Coq proof assistant. We also show that Laugwitz-Schmieden numbers can be used to actually compute continuous functions. We hope that this work could improve techniques for both implementing numeric computations and reasoning about them in geometric systems.

Keywords: formal proofs, discrete geometry, non-standard arithmetic, arithmetisation scheme, exact computations, Coq
[3] Éric Andres, Marie-Andrée Da Col, Laurent Fuchs, Gaëlle Largeteau-Skapin, Nicolas Magaud, Loïc Mazo, and Rita Zrour. Les Ω-AQA : Représentation discrète des applications affines. In Nicolas Passat, editor, Neuvièmes journées du Groupe de Travail de Géométrie Discrète (GéoDis 2014), Nov. 2014. Presented at ReimsImage'2014 http://reimsimage2014.univ-reims.fr/geodis-2014/sessions/. [ bib | .pdf ]
La droite d'Harthong-Reeb est un modèle numérique du continu basé sur les entiers. La construction de cette droite en utilisant les Ω-entiers permet de décrire les objets mathématiques réels de manière discrète et constructive. En informatique graphique on est souvent amené à transformer des objets (images) par des applications affines réelles (rotations, translations, similitudes,...). Des discrétisés (à une échelle donnée) de ces applications, appelées applications quasi-affines ont été définies et étudiées. Dans ce papier, nous rappelons les définitions et propriétés de base des Ω-entiers, de la droite de Harthong-Reeb et des applications quasi-affines. Nous montrons ensuite comment définir des Ω-AQAs qui sont les discrétisés multi-échelle des applications affines suivant la théorie des Ω-entiers et la définition initiale des AQAs. Enfin nous donnons les premières propriétés de ces Ω-AQAs.

[4] Bruno Cuervo Parrino, Julien Narboux, Eric Violard, and Nicolas Magaud. Dealing with arithmetic overflows in the polyhedral model. In Uday Bondhugula and Vincent Loechner, editors, 2nd International Workshop on Polyhedral Compilation Techniques (IMPACT'2012), Jan. 2012. Accepted for presentation at the workshop. [ bib | http ]
The polyhedral model provides techniques to optimize Static Control Programs (SCoP) using some complex transformations which improve data-locality and which can exhibit parallelism. These advanced transformations are now available in both GCC and LLVM. In this paper, we focus on the correctness of these transformations and in particular on the problem of integer overflows. Indeed, the strength of the polyhedral model is to produce an abstract mathematical representation of a loop nest which allows high-level transformations. But this abstract representation is valid only when we ignore the fact that our integers are only machine integers. In this paper, we present a method to deal with this problem of mismatch between the mathematical and concrete representations of loop nests. We assume the existence of polyhedral optimization transformations which are proved to be correct in a world without overflows and we provide a self-verifying compilation function. Rather than verifying the correctness of this function, we use an approach based on a validator, which is a tool that is run by the compiler after the transformation itself and which confirms that the code produced is equivalent to the original code. As we aim at the formal proof of the validator we implement this validator using the Coq proof assistant as a programming language.

[5] Christophe Brun, Jean-François Dufourd, and Nicolas Magaud. Formal Proof in Coq and Derivation of a Program in C++ to Compute Convex Hulls. In Tetsuo Ida and Jacques D. Fleuriot, editors, Automated Deduction in Geometry (ADG'2012) - Revised Selected Papers, volume 7993 of LNCS, pages 71--88. Springer, 2012. ISBN 978-3-642-40671-3. [ bib | http ]
This article presents a generic method to build programs in computational geometry from their specifications. It focuses on a case study namely computing incrementally the convex hull of a set of points in the plane. Our program to compute convex hulls is specified and proved correct using the Coq proof assistant. A concrete implementation in Ocaml is then automatically extracted and an efficient C++ program is derived (by hand) from the specification.

[6] Nicolas Magaud, Agathe Chollet, and Laurent Fuchs. Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective. In Automated Deduction in Geometry (ADG'2010), pages 1--17, 2010. Accepted for presentation at the conference. An extended version is published in an international journal [2]. [ bib | http | .pdf ]
This work presents a formalization of the discrete model of the continuum introduced by Harthong and Reeb, the Harthong-Reeb line. This model was at the origin of important developments in the Discrete Geometry field. The formalization is based on a previous work by some of the authors where it was shown that the Harthong-Reeb line satisfies the axioms for constructive real numbers introduced by Bridges. A formalization of a first attempt for a model of the Hartong-Reeb line based on the work of Laugwitz and Schmieden is also presented and analyzed. We hope that this work could help reasoning and implementation of numeric computations in geometric systems.

[7] Nicolas Magaud, Julien Narboux, and Pascal Schreck. A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem. Computational Geometry: Theory and Applications, 45(8):406--424, 2012. [ bib | http ]
Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to formalize fairly easily Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space.

Keywords: formalization, projective geometry, Coq, rank, desargues, hessenberg, hexamy
[8] Christophe Brun, Jean-François Dufourd, and Nicolas Magaud. Designing and Proving Correct a Convex Hull Algorithm with Hypermaps in Coq. Computational Geometry: Theory and Applications, 45(8):436--457, 2012. [ bib | http ]
This article presents the formal design of a functional algorithm which computes the convex hull of a finite set of points incrementally. This algorithm, specified in Coq, is then automatically extracted into an OCaml-program which can be plugged into an interface for data input (point selection) and graphical visualization of the output. A formal proof of total correctness, relying on structural induction, is also carried out. This requires to study many topologic and geometric properties. We use a combinatorial structure, namely hypermaps, to model planar subdivisions of the plane. Formal specifications and proofs are carried out in the Calculus of Inductive Constructions and its implementation: the Coq system.

[9] Nicolas Magaud, Julien Narboux, and Pascal Schreck. Formalizing Desargues' Theorem in Coq using Ranks. In Proceedings of the ACM Symposium on Applied Computing SAC 2009, pages 1110--1115. ACM, ACM Press, March 2009. [ bib | http ]
Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions leads to technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this paper, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. It allows to carry out proofs in a more systematic way. To validate this approach, we formalize in Coq (using only ranks) one of the fundamental theorems of the projective space, namely Desargues' theorem.

[10] Nicolas Magaud, Julien Narboux, and Pascal Schreck. Formalizing Projective Plane Geometry in Coq. In Thomas Sturm, editor, Post-proceedings of ADG'2008, volume 6301 of LNAI. Springer, 2008. [ bib | http ]
We investigate how projective plane geometry can be formalized in a proof assistant such as Coq. Such a formalization increases the reliability of textbook proofs whose details and particular cases are often overlooked and left to the reader as exercises. Projective plane geometry is described through two different axiom systems which are formally proved equivalent. Usual properties such as decidability of equality of points (and lines) are then proved in a constructive way. The duality principle as well as formal models of projective plane geometry are then studied and implemented in Coq. Finally, notions of flats and ranks are introduced and their basic properties are proved. This would allow to develop a more algebraic approach to proofs of alignment properties such as Desargues' theorem.

[11] Manuel M.T. Chakravarty, Nicolas Magaud, and Don Stewart. Machine-Independent Code Certification with the LF Type Theory. In Dependently Typed Programming 08, Feb. 2008. A TYPES (small) topical workshop. [ bib | http ]
Code certification is usually investigated for architecture-dependent assembly or machine code, where the trusted computing base (TCB) is minimised at the expense of portability. Work that departs from that scheme typically focuses on a comparatively high-level abstract machine code, such as that of the Java Virtual machine. In contrast, the aim of this work is machine-independent certified code on a level that is just above that of an architecture-dependent code. In other words, we aim to minimise the TCB under the over- ruling aim of portability. We represent computations as terms of a polymorphic lambda calculus in administrative normal form, which essentially is a low- level intermediate language. The type structure of these terms is embedded in the dependently-typed LF type theory, which serves to represent certificates. We study how to show the resulting type system is sound and that the operational semantics of the calculus does not depend on (dependent) type information. Moreover, we have implemented a prototype compiler that compiles a small functional language into certified code as well as a prototype certificate checker based on Twelf.

[12] Christophe Brun, Jean-François Dufourd, and Nicolas Magaud. Enveloppes convexes et cartes combinatoires en Coq. In Journées Informatique et Géometrie, INRIA Sophia-Antipolis, June 2007. [ bib | http | .pdf ]
[13] Nicolas Magaud. Programming with Dependent Types in Coq: a Study of Square Matrices, Jan 2005. Unpublished. A preliminary version appeared in Coq contributions. [ bib | http ]
The Coq proof system allows users to write (functional) programs and to reason about them in a formal way. We study how to program using dependently typed data structures in such a setting. Using dependently typed data structures enables programmers to have more precise specifications for their programs before starting proving any significant properties (e.g. total correctness) about these programs. We particularly focus on an operational description of square matrices and their operations. Matrices are represented using dependent types. A matrix is a vector of rows, which are themselves vectors indexed by natural numbers. We also take advantage of Coq modules system to have matrices parametrised by a carrier set. Finally, this operational description of square matrices can be extracted into a mainstream functional programming language like Ocaml.

[14] Nicolas Magaud. Dependently Typed Programming in the Coq Proof Assistant. In Dependently Typed Programming: Dagsthul Seminar 04381, Dagsthul, September 2004. An overview of the current programming techniques in Coq. [ bib | .pdf ]
[15] Nicolas Magaud. Changements de Représentation des Données dans le Calcul des Constructions. PhD thesis, Université de Nice Sophia-Antipolis, October 2003. [ bib | http | .pdf ]
Nous étudions comment faciliter la réutilisation des preuves formelles en théorie des types. Nous traitons cette question lors de l'étude de la correction du programme de calcul de la racine carrée de GMP. A partir d'une description formelle, nous construisons un programme impératif avec l'outil Correctness. Cette description prend en compte tous les détails de l'implantation, y compris l'arithmétique de pointeurs utilisée et la gestion de la mémoire.
Nous étudions aussi comment réutiliser des preuves formelles lorsque l'on change la représentation concrète des données. Nous proposons un outil qui permet d'abstraire les propriétés calculatoires associées à un type inductif dans les termes de preuve. Nous proposons également des outils pour simuler ces propriétés dans un type isomorphe. Nous pouvons ainsi passer, systématiquement, d'une représentation des données à une autre dans un développement formel.

[16] Nicolas Magaud. Changing Data Representation within the Coq System. In TPHOLs'2003, volume 2758 of LNCS. Springer-Verlag, 2003. [ bib | http | .pdf ]
In a theorem prover like Coq, mathematical concepts can be implemented in several ways. Their different representations can be either efficient for computing or well-suited to carry out proofs easily. In this paper, we present improved techniques to deal with changes of data representation within Coq. We propose a smart handling of case analysis and definitions together with some general methods to transfer recursion operators and their reduction rules from one setting to another. Once we have built a formal correspondence between two settings, we can translate automatically properties obtained in the initial setting into new properties in the target setting. We successfully experiment with changing Peano's numbers into binary numbers for the whole 'Arith' library of Coq as well as with changing polymorphic lists into reversed (snoc) lists.

[17] Yves Bertot, Nicolas Magaud, and Paul Zimmermann. A Proof of GMP Square Root. Journal of Automated Reasoning, 29(3-4):225--252, 2002. Special Issue on Automating and Mechanising Mathematics: In honour of N.G. de Bruijn. An earlier version is available as a research report [18]. [ bib ]
We present a formal proof (at the implementation level) of an efficient algorithm proposed by Paul Zimmermann to compute square roots of arbitrarily large integers. This program, which is part of the GNU Multiple Precision Arithmetic Library (GMP), is completely proven within the Coq system. Proofs are developed using the Correctness tool to deal with imperative features of the program. The formalization is rather large (more than 13000 lines) and requires some advanced techniques for proof management and reuse.

[18] Yves Bertot, Nicolas Magaud, and Paul Zimmermann. A Proof of GMP Square Root using the Coq Assistant. Research report 4475, INRIA, June 2002. Research Report INRIA. [ bib | http ]
[19] Nicolas Magaud and Yves Bertot. Changing data structures in type theory:a study of natural numbers. In Paul Callaghan, Zhaohui Luo, James McKinna, and Randy Pollack, editors, Post-proceedings of TYPES'2000, volume 2277 of LNCS. Springer-Verlag, 2002. [ bib | http | .pdf ]
In type-theory based proof systems that provide inductive structures, computation tools are automatically associated to inductive definitions. Choosing a particular representation for a given concept has a strong influence on proof structure. We propose a method to make the change from one representation to another easier, by systematically translating proofs from one context to another. We show how this method works by using it on natural numbers, for which a unary representation (based on Peano axioms) and a binary representation are available. This method leads to an automatic translation tool that we have implemented in Coq and successfully applied to several arithmetical theorems.

[20] Nicolas Magaud and Yves Bertot. Changements de Représentation des Structures de Données en Coq: le cas des Entiers Naturels. In JFLA'2001, 2001. Also available as INRIA Research Report [22]. [ bib | .pdf ]
Dans le calcul des constructions inductives, des outils de calcul et de preuve sont associés à chaque type de données concret défini inductivement. Par conséquent, le choix d'une structure de données influence fortement le contenu des preuves. Nous proposons dans ce document une méthode pour passer facilement d'une représentation à une autre, en effectuant des traductions partiellement automatisées des preuves. Nous mettons cette méthode en œuvre sur les entiers naturels, pour lesquels il existe une représentation unaire (à la Peano) et une représentation binaire. Un prototype d'outil de traduction est développé dans le système Coq et a été expérimenté avec succès sur une dizaine de théorèmes d'arithmétique.

[21] Jean-Christophe Filliâtre and Nicolas Magaud. Certification of Sorting Algorithms in the Coq System. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999. [ bib | .pdf ]
We present the formal proofs of total correctness of three sorting algorithms in the Coq system, namely insertion sort, quicksort and heapsort. The implementations are imperative programs working in-place on a given array. Those developments demonstrate the usefulness of inductive types and higher-order logic in the process of software certification. They also show that the proof of rather complex algorithms may be done in a small amount of time --- only a few days for each development --- and without great difficulty.

[22] Nicolas Magaud and Yves Bertot. Changements de Représentation des Données dans le Calcul des Constructions Inductives. Rapport de recherche 4039, INRIA, Octobre 2000. [ bib | http ]
[23] Nicolas Magaud. Structures de Données Abstraites dans le Calcul des Constructions Inductives. Rapport de stage de DEA, Université de Nice Sophia-Antipolis, Juin 2000. [ bib | .pdf ]
[24] Nicolas Magaud. Preuve de Correction d'un Traducteur de Code Java vers JavaCard dans le système Coq. Rapport de stage de deuxième année de Magistère Informatique et Modélisation, Ecole Normale Supérieure de Lyon, Août 1999. [ bib | .pdf ]
[25] Nicolas Magaud. Preuve de Programmes Impératifs dans le Système Coq : Tri par Insertion d'un Tableau. Rapport de stage de première année de Magistère Informatique et Modélisation, Ecole Normale Supérieure de Lyon, Juillet 1998. [ bib | .pdf ]

This file was generated by bibtex2html 1.98.