Academic Positions

  • Present 2024

    Maître de conférences[W]

    University of Strasbourg

  • 2024 2024

    Research engineer

    University of Strasbourg

  • 2023 2021

    Research engineer

    Inria, Sophia Antipolis

  • 2021 2019

    Postdoctoral researcher

    Inria, Sophia Antipolis

Education & Training

  • 2018 2013

    Ph.D. degree, On the Formalization of Foundations of Geometry

    University of Strasbourg

  • 2013 2011

    M.Sc. degree, Engineering Mathematics and Computational Science

    Chalmers University of Technology, Gothenburg

  • 2011 2009

    Engineering degree, M.Sc. degree equivalent

    ENSIIE, Strasbourg

Main Co-Authors

Gabriel Braun

Associate Professor

His Web page

Pascal Schreck

Professor

His Web page

Julien Narboux

Associate Professor

His Web page

Danijela Simić

Assistant Professor

Her Web page

Filip Marić

Professor

His Web page

Bruno Blanchet

Senior Researcher

His Web page

Christian Doczkal

Postdoctoral Researcher

His Web page

Benjamin Grégoire

Researcher

His Web page

Pierre-Yves Strub

Researcher

His Web page

Michael Beeson

Professor Emeritus

His Web page

Filter by type:

Sort by year:

CV2EC: Getting the Best of Both Worlds

Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub
Conference PaperCSF 2024 - 37th IEEE Computer Security Foundations Symposium, IEEE, Jul 2024, Enschede, Netherlands. pp.283-298.

Abstract

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.

Towards an Independent Version of Tarski's System of Geometry

Pierre Boutry, Stéphane Kastenbaum, Clément Saintier
Conference PaperPedro Quaresma and Zoltán Kovács. Proceedings 14th International Conference on Automated Deduction in Geometry, Belgrade, Serbia. pp. 73–84, 2023, Proceedings of ADG 2023.

Abstract

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.

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Danijela Simić, Filip Marić, Pierre Boutry
Journal PaperJournal of Automated Reasoning, Springer Verlag, 2020.

Abstract

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.

Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq

Charly Gries, Julien Narboux, Pierre Boutry
Conference PaperLes trentèmes Journées Francophones des Langages Applicatifs (JFLA 2019), Jan 2019, Les Rousses, France. 2019, Actes des Trentièmes Journées Francophones des Langages Applicatifs (JFLA 2019).

Abstract

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.

On the Formalization of Foundations of Geometry

Pierre Boutry
ThesisPh.D. thesis, Université de Strasbourg, 2018.

Abstract

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.

Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq

Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck
Journal PaperJournal of Automated Reasoning, Springer Verlag, 2017.

Abstract

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.

Formalization of the Arithmetization of Euclidean Plane Geometry and Applications

Pierre Boutry, Gabriel Braun, Julien Narboux
Journal PaperJournal of Symbolic Computation, Elsevier, 2017, Special Issue on Symbolic Computation in Software Science.

Abstract

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.

From Hilbert to Tarski

Gabriel Braun, Pierre Boutry, Julien Narboux
Conference PaperJulien Narboux, Pascal Schreck and Ileana Streinu. Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp. 78–96, 2016, Proceedings of ADG 2016.

Abstract

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.

From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry

Pierre Boutry, Gabriel Braun, Julien Narboux
Conference PaperSCSS 2016 The 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan.

Abstract

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.

Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq

Charly Gries, Pierre Boutry, Julien Narboux
Conference PaperLes vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint Malo, France. 2016, Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016).

Abstract

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.

A reflexive tactic for automated generation of proofs of incidence to an affine variety

Pierre Boutry, Julien Narboux, Pascal Schreck
Unpublished Paper

Abstract

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.

Herbrand's theorem and non-Euclidean geometry

Michael Beeson, Pierre Boutry, Julien Narboux
Journal PaperBulletin of Symbolic Logic, Association for Symbolic Logic, 2015, 21 (2), pp. 111-122.

Abstract

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.

A short note about case distinctions in Tarski's geometry

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun
Conference PaperFrancisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp. 51–65, 2014, Proceedings of ADG 2014.

Abstract

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.

Using small scale automation to improve both accessibility and readability of formal proofs in geometry

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun
Conference PaperFrancisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp. 31–49, 2014, Proceedings of ADG 2014.

Abstract

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.

Teaching History

  • 2025 2023

    Computability and complexity

    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.

  • 2025 2023

    Introduction to formal language and proofs

    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.

  • 2025 2024

    Arithmetic and cryptography

    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.

  • 2025 2024

    Computer-assisted proofs

    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.

  • 2025 2024

    Functional programming

    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.

  • 2025 2024

    Logic and logic programming

    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.

  • 2017 2014

    Mathematical logic

    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.

  • 2017 2016

    Functional programming

    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.

  • 2017 2016

    Mathematical tools

    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.

  • 2017 2016

    Proof engineering

    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.

  • 2016 2013

    Numerical analysis

    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.

  • 2016 2015

    Imperative programming

    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.

  • 2014 2013

    Operations research

    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.