I am an associate professor[W] (maître de conférences[W]) at the Department of Mathematics and Computer Science of the University of Strasbourg. I belong to the IGG team of the ICube Laboratory.
Prior to this, I was a postdoctoral researcher and a research engineer at Inria in the STAMP team and later at the University of Strasbourg in the IGG team.
I was a Ph.D. student at the University of Strasbourg. I was a member of the IGG team of the ICube Laboratory. My work was supervised by Julien Narboux and directed by Pascal Schreck.
My principal interests of research are in formalization and foundations of geometry[W].
I am mostly interested in the foundations of geometry[W] and their formalization within the Coq system using the Mathematical Components library. I obtained a Ph.D. on ways to axiomatize Euclidean geometry, statements of the parallel postulate and the possibilities of automating geometric reasoning. I have notably contributed to the discovery of a new proof of the independence of the parallel postulate.
I am one of the authors of the CV2EC tool. It allows to translate CryptoVerif assumptions to EasyCrypt games[1, 2]. As part of the Formosa Crypto project, I worked on building a formally verified model of Curve25519[W] which led to the ongoing effort of developing a field extension[W] library for EasyCrypt.
Most of my work corresponds to Coq or Isabelle formalizations available with the GeoCoq library or the Poincaré Disc Model entry of the Archive of Formal Proofs. I also contributed to CryptoVerif and EasyCrypt.
While it does not seem to collect all of my publications, my DBLP[W] page could contain my latest publications in case I did not update this page recently enough.
Besides my publications, you can find the abstract of my invited talk at the Logic Colloquium 2019 in The Bulletin of Symbolic Logic, the slides and the exercises from the computer lab session that Julien Narboux and I presented during our invited GeoCoq tutorial at ADG 2023, and a review of one of my papers in zbMATH[W].
We define and implement CV2EC, a translation from CryptoVerif assumptions on primitives to EasyCrypt games. CryptoVerif and EasyCrypt are two proof tools for mechanizing game-based proofs. While CryptoVerif is primarily suited for verifying security protocols, EasyCrypt has the expressive power for verifying cryptographic primitives and schemes. CV2EC allows us to prove security protocols in CryptoVerif and then use EasyCrypt to prove the assumptions made in CryptoVerif, either directly or by reducing them to lower-level or more standard cryptographic assumptions. We apply this approach to several case studies: we prove the multikey computational and gap Diffie-Hellman assumptions used in CryptoVerif from the standard version of these assumptions; we also prove an n-user security property of authenticated key encapsulation mechanisms (KEMs), used in the CryptoVerif study of hybrid public-key encryption (HPKE), from the 2-user version. By doing that, we discovered errors in the paper proof of this property, which we reported to the authors who then fixed their proof.
In 1926-1927, Tarski designed a set of axioms for Euclidean geometry which reached its final form in a manuscript by Schwabhäuser, Szmielew and Tarski in 1983. The differences amount to simplifications obtained by Tarski and Gupta. Gupta presented an independent version of Tarski's system of geometry, thus establishing that his version could not be further simplified without modifying the axioms. To obtain the independence of one of his axioms, namely Pasch's axiom, he proved the independence of one of its consequences: the previously eliminated symmetry of betweenness. However, an independence model for the non-degenerate part of Pasch's axiom was provided by Szczerba for another version of Tarski's system of geometry in which the symmetry of betweenness holds. This independence proof cannot be directly used for Gupta's version as the statements of the parallel postulate differ. In this paper, we present our progress towards obtaining an independent version of a variant of Gupta's system. Compared to Gupta's version, we split Pasch's axiom into this previously eliminated axiom and its non-degenerate part and change the statement of the parallel postulate. We verified the independence properties by mechanizing counter-models using the Coq proof-assistant.
We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line ℂP1 and is shown to satisfy Tarski's axioms except for Euclid's axiom — it is shown to satisfy it's negation, and, moreover, to satisfy the existence of limiting parallels axiom.
Dans cet article, nous présentons les résultats sur la continuité que nous avons obtenus dans le cadre du projet GeoCoq, qui constitue une formalisation en Coq de la géométrie : nous avons défini 11 axiomes de continuité et établi leur hiérarchie. Nos démonstrations ont été formalisées dans le cadre de la géométrie neutre de Tarski en dimension quelconque et de la logique intuitionniste.
In this thesis, we investigate how a proof assistant can be used to study the foundations of geometry. We start by focusing on ways to axiomatize Euclidean geometry and their relationship to each other. Then, we expose a new proof that Euclid's parallel postulate is not derivable from the other axioms of first-order Euclidean geometry. This leads us to refine Pejas' classification of parallel postulates. We do so by considering decidability properties when classifying the postulates. However, our intuition often guides us to overlook uses of such properties. A proof assistant allows us to use a perfect tool which possesses no intuition: a computer. Moreover, proof assistants let us leverage the computational capabilities of computers. We demonstrate how we enable the use of algebraic automated deduction methods thanks to the arithmetization of geometry. Finally, we present a specific procedure designed to automate proofs of incidence properties.
In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid's 5 th postulate. Our study is performed in the context of Tarski's neutral geometry, or equivalently in Hilbert's geometry defined by the first three groups of axioms, and uses an intuitionistic logic, assuming excluded-middle only for point equality. Our formalization provides a clarification of the conditions under which different versions of the postulates are equivalent. Following Beeson, we study which versions of the postulate are equivalent , constructively or not. We distinguish four groups of parallel postulates. In each group, the proof of their equivalence is mechanized using intuitionistic logic without continuity assumptions. For the equivalence between the groups additional assumptions are required. The equivalence between the 34 postulates is formalized in Archimedean planar neutral geometry. We also formalize a theorem due to Szmiliew. This theorem states that, assuming Archimedes' axiom, any statement which hold in the Euclidean plane and does not hold in the Hyperbolic plane is equivalent to Euclid's 5 th postulate. To obtain all these results, we have developed a large library in planar neutral geometry, including the formalization of the concept of sum of angles and the proof of the Saccheri-Legendre theorem, which states that assuming Archimedes' axiom, the sum of the angles in a triangle is at most two right angles.
This paper describes the formalization of the arithmetization of Euclidean plane geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamath-ematical properties. This work completes our formalization of the two-dimensional results contained in part one of the book by Schwabhäuser Szmielew and Tarski Metamathematische Methoden in der Geometrie. We defined the arithmetic operations geometrically and proved that they verify the properties of an ordered field. Then, we introduced Cartesian coordinates, and provided characterizations of the main geometric predicates. In order to prove the characterization of the segment congruence relation, we provided a synthetic formal proof of two crucial theorems in geometry, namely the intercept and Pythagoras' theorems. To obtain the characterizations of the geometric predicates, we adopted an original approach based on bootstrapping: we used an algebraic prover to obtain new characterizations of the predicates based on already proven ones. The arithmetization of geometry paves the way for the use of algebraic automated deduction methods in synthetic geometry. Indeed, without a " back-translation " from algebra to geometry, algebraic methods only prove theorems about polynomials and not geometric statements. However, thanks to the arithmetization of geometry, the proven statements correspond to theorems of any model of Tarski's Euclidean geometry axioms. To illustrate the concrete use of this formalization, we derived from Tarski's system of geometry a formal proof of the nine-point circle theorem using the Gröbner basis method. Moreover , we solve a challenge proposed by Beeson: we prove that, given two points, an equilateral triangle based on these two points can be constructed in Euclidean Hilbert planes. Finally, we derive the axioms for another automated deduction method: the area method.
In this paper, we describe the formal proof using the Coq proof assistant that Tarski's axioms for plane neutral geometry (excluding continuity axioms) can be derived from the corresponding Hilbert's axioms. Previously, we mechanized the proof that Tarski's version of the parallel postulate is equivalent to the Playfair's postulate used by Hilbert and that Hilbert's axioms for plane neutral geometry (excluding continuity) can be derived from the corresponding Tarski's axioms. Hence, this work allows us to complete the formal proof of the equivalence between the two axiom systems for neutral and plane Euclidean geometry. Formalizing Hilbert's axioms is not completely straightforward, in this paper we describe the corrections we had to make to our previous formalization. We mechanized the proof of Hilbert's theorems that are required in our proof of Tarski's axioms. But this connection from Hilbert's axioms, allows to recover the many results we obtained previously in the context of Tarski's geometry: this includes the theorems of Pappus, Desargues, Pythagoras and the arithmetization of geometry.
This paper describes the formalization of the arithmetization of Euclidean geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamathematical properties. This work completes our formalization of the two-dimensional results contained in part one of [SST83]. We defined the arithmetic operations geometrically and proved that they verify the properties of an ordered field. Then, we introduced Cartesian coordinates, and provided characterizations of the main geometric predicates. In order to prove the characterization of the segment congruence relation, we provided a synthetic formal proof of two crucial theorems in geometry, namely the intercept and Pythagoras' theorems. To obtain the characterizations of the geometric predicates, we adopted an original approach based on bootstrapping: we used an algebraic prover to obtain new characterizations of the predicates based on already proven ones. The arithmetization of geometry paves the way for the use of algebraic automated deduction methods in synthetic geometry. Indeed, without a " back-translation " from algebra to geometry, algebraic methods only prove theorems about polynomials and not geometric statements. However, thanks to the arithmetization of geometry, the proven statements correspond to theorems of any model of Tarski's Euclidean geometry axioms. To illustrate the concrete use of this formalization, we derived from Tarski's system of geometry a formal proof of the nine-point circle theorem using the Gröbner basis method.
Nous nous intéressons dans cet article au 5e postulat d'Euclide. Ce postulat a une importance historique : pendant des siècles, de nombreux mathématiciens de renom ont cru que cet axiome était un théorème qui pouvait être dérivé des quatre premiers postulats d'Euclide. Dans cet article nous présentons la formalisation en Coq de résultats concernant le lien entre l'unicité de la parallèle et le fait que la somme des angles d'un triangle est égale à deux droits. Nous travaillons en logique intuitionniste dans le contexte de l'axiomatique de Tarski. D'une part nous obtenons la preuve formelle de l'équivalence et d'autre part nous clarifions les propriétés de décidabilité nécessaires pour la preuve. Nous étudions également le lien entre l'axiome d'Aristote et la décidabilité de l'intersection entre deux droites.
This paper describes the formalization and implementation of a reflexive tactic for automated generation of proofs of incidence to an affine variety. Incidence proofs occur frequently in formal proofs of geometric statements. Nevertheless they are most of the time omitted in pen-and-paper proofs since they do not contribute to the understanding of the proof in which they appear. Our tactic allows us to automate proofs about incidence to an affine variety. Being based on a type class capturing the minimal set of properties needed to deal with incidence, the tactic is applicable to any theory verifying these properties. This type class is defined using dependent types to formalize predicates of parameterizable arity which represent the incidence to an affine variety.
We use Herbrand's theorem to give a new proof that Euclid's parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.
In this paper we study some decidability properties in the context of Tarski's axiom system for geometry. We removed excluded middle from our assumptions and studied how our formal proofs of the first thirteen chapters of [SST83] were impacted. We show that decidability of equality is equivalent to the decidability of the two other given predicates of the theory: congruence and betweenness. We prove that the decidability of the other predicates used in [SST83] can be derived except for the predicate stating the existence of the intersection of two lines. All results have been proved formally using the Coq proof assistant.
This paper describes some techniques to help building formal proofs in geometry and at the same time improving readability. Rather than trying to completely automate the proving process we provide symbolic manipulations which are useful to automate the parts of the formal proof that are usually implicit in a pen and paper proof. We test our framework using some well known theorems about triangles which are taught in high-school. We also highlight the proof steps which are usually overlooked in informal proofs and that we believe should be made explicit. Our framework is based on Tarski's geometry within the Coq proof assistant, but most of the ideas presented in this paper could be applied to other axiomatic systems or proof assistants.
While I was not at a university, I was still teaching at Inria Academy, a continuing education program dedicated to open source software, where, together with Yves Bertot, we created modules to teach the use of the Coq proof assistant.
The most general models of computation are described: Turing machines, context-sensitive grammars and general recursive functions. The significance of non-determinism in computation is explained. The limits of these models are then given, showing the undecidability of some decision problems, such as the halting problem. Finally, the complexity classes P, NP and EXP, are given, with particular emphasis on NP-complete problems.
This course is an introduction to the mathematical language and mathematical proofs. It covers elementary logic, proof techniques (direct, contraposition, reductio ad absurdum), basic set theory, fundamental properties of ℕ and mathematical induction.
The course consists of two parts. During the first part, basic number theory concepts (divisibility, Bézout's identity, Euclidean algorithm, prime numbers), modular arithmetic (ring of integers modulo m, Euler's totient function, Fermat's little theorem, Euler's theorem, modular exponentiation) and the Chinese remainder theorem are studied. The second part focuses on public-key cryptosystem (RSA), key exchange (Diffie-Hellman, ElGamal), private-key cryptosystem (AES), hash algorithm (SHA-256) and applications to crypto-currencies.
The course serves as an introduction to the tools for formal proofs and certification of softwares through the use of the Coq proof assistant. It presents the motivations and some examples of the use of proof assistants, proofs in propositional and predicate calculus, tactic-based interaction, algebraic data types, inductive data types, inductive predicates, pattern matching, functional recursion, mathematical induction, polymorphism, implicit arguments, higher-order functions, the Brouwer-Heyting-Kolmogorov interpretation and the Curry-Howard correspondence.
This course covers the functional programming paradigm, its founding principles (function composition, variables in the mathematical sense, referential transparency property, purity), the basic concepts for writing a program in this mode (functional equation, function application, conditionals, anonymous function, temporary definition, recursion), as well as more advanced notions (functional, higher-order functions, curryfication, partial application). The types ubiquitous in recent functional languages are studied (algebraic data types, pattern matching, polymorphism, type inference). Different evaluation strategies (eager/lazy evaluation) for functional expressions are discussed.
This course is an introduction to logic and its relationship to computer science. It introduces the logic programming paradigm through the use of the Prolog language. During this course, propositional and predicate calculus (syntax and semantics), formal systems (soundness and completeness), natural deduction, conversion to clausal, prenex and Skolem normal form, unification, resolution for predicate calculus and an introduction to Prolog are studied.
The goal of the course is to present inductively defined sets, proofs by induction, propositional and first-order logic and resolution. In addition, the soundness and completeness of the rules of both propositional and first-order logic is demonstrated.
The course covers the principles and pratice of programming in a functional language, illustrated with the use of the OCaml language. Its aim is to introduces the functional kernel of the OCaml language, exception handling, sum types, inductive types, recursion, higher-order functions and modules while emphasising the notion of persistent data structure. These concepts are practiced through the study of different implementations of sets as lists, binary search trees or AVL trees as well as maps and suffix trees.
The aim of the course is to give to students with a background in computer science the opportunity to obtain a reliable basis in mathematics. The different lessons focus on the most crucial mathematical concepts for a future engineer: functions of a real variable, complex numbers, polynomials, matrices, matrix diagonalization, integral calculus, Taylor series, integrability, numeric sequences and series, power series.
The course serves as an introduction to the tools for formal proofs and certification of softwares through the use of the Coq proof assistant. It covers the definition of types, functions, propositions, the relationship between mathematics and programming, definitions and proofs by induction as well as notions of certification and program extraction from proofs.
The course consists of two parts. During the first part, basic linear algebra concepts like matrix algebra, vector and matrix norms, error analysis or condition numbers, several variants of Gaussian elimination, some stationary iterative methods and analysis of algorithms are studied. The second part focuses on numerical methods for ordinary differential equations and their analysis.
This is an introductory course in programming, using the imperative language C as the medium of instruction. It describes the concepts of variables, iterative and recursive algorithms, iterations, functions, IO and streams, file management, standard and external librairies, memory allocation, pointer and pointer arithmetic. Moreover, it gives an overview of sorting algorithms and data structures such as vectors, string, lists, trees or binary search trees.
The course is divided into two parts. The first part provides an introduction to linear programming, branch-and-bound algorithms, dynamic programming and algorithms for shortest path problems, scheduling and flow problems. The second part covers stochastic processes, queueing theory and inventory theory.
I would be happy to talk to you about my research or to answer questions regarding the courses in which I teach. You can find me at either of the following places.
ICube Laboratory
Pôle API
BP 10413
300 Bd Sébastien Brant
67412 Illkirch cedex
FRANCE
Office C118
UFR Math-Info
UFR de mathématique et d'informatique
7 Rue René Descartes
67000 Strasbourg
FRANCE
Office 302
