Les démonstrations mathématiques, EllipsesIntroduction à la logique, Dunod

Articles in journal and proceedings, prepuplications

Isotopic piecewise affine approximation of algebraic varieties (2023). Prepublication on ArXiv (download pdf)
On a question of supports, with Frédéric Mangolte (2022). European Journal of Mathematics, Volume 8, Issue 3, pages 1036-1041. Download pdf.
Computational contents of classical logic and extensional choice. pdf
Practical Subtyping for Curry-Style Languages with Rodolphe Lepigre, in ACM Transactions On Programming Languages And System (TOPLAS), Volume 41, Issue 1, pages 575-631, 2019.
Abstract Representation of Binders in OCaml using the Bindlib Library with Rodolphe Lepigre, proceedings of Logical Frameworks and Meta-Languages: Theory and Practice, EPTCS Volume 274, pages 42-56, 2018.
Les démonstrations mathématiques with René David, Pierre Hyvernat and Karim Nour, Ellipses, 2017, ISBN : 9782340016668.
Mêler combinateurs, continuations et EBNF pour une analyse syntaxique efficace en OCaml with Rodolphe Lepigre, 2014 available in pdf
Asymptotically almost all λ-terms are strongly normalizing with René David, Guillaue Theyssier, Katarzyna Grygiel, Jakub Kozik and Marek Zaionc, in LMCS Volume 9, Issue 1, 2013 available in pdf
Distance to the discriminant. in preparation, pdf.
Nullstellensatz and positivestellensatz from cut-elimination (draft available in pdf.
Improvements on the "Size Change Termination Principle" in a functional language with Pierre Hyvernat, abstract of the talk to be presented at WST2010 at Edinburgh, available in pdf.
Realizability for programming languages. (hal-00474043), available in pdf. The paper contains the source of the presented algorithm with some boring parts removed. If you want to compile the toyML interpreter, you can download the complete source.
MathNat - Mathematical Text in a Controlled Natural Language with Muhammad Humayoun, available in pdf (proceedings of Cicling 2010, Roumania)
Realizability of the axiom of choice in HOL (An analysis of Krivines's work) with Frédéric Ruyer in Fundamenta Informaticae Volume 84 Issue 2, (2008) pages 241-258. Download: pdf
PhoX with Paul Rozière in The seventeen provers of the World Freek Wiedijk (editor) LNAI 3600 pages 67-71.
System ST Schedae Informatica, proceedings of the Chambery-Krawow-Lyon Workshop, Vol. 12, pages 97-112 (June 2003)
GlSurf, Maths et Dessins en OCaml, (2003). JFLA 2004. Download: pdf.
Getting results from programs extracted from classical proofs, TCS 2004, volume 323, pages 49-70. note: you can also download the formalized proof of Dickson's lemma in PhoX (three files needed to run the program in PhoX: dickson.phx, storage.phx and run_dickson.phx). You can also download a program in OCaml extracted "by hand". Download: pdf.
System St, beta-reduction and completeness, presented at LICS 2003, publication IEEE, pages 21-32. Formal proofs in PhoX available. Download pdf.
Computer Assisted Teaching in Mathematics, with René David, to appear in the proceedings of the Workshop on 35 years of Automath (Avril 2002, Edingurgh) (this is an english version of (Raf01c) with amelioration). Download pdf.
System St, toward a Type System for Extraction and Proof of Programs, Archive for Pure and Applied Logic, 2003, volume 122, pages 107-130. Formal proofs in PhoX available. Download: pdf.
Apprentissage du raisonnement assité par ordinateur, with René David, Quadrature numéro 45, printemps 2002, pages 25-36). Downloaad pdf.

Version courte parue dans la gazette de la SMF, avril 2002, numéro 92, pages 48-56. Downloaad pdf.

Introduction à la Logique, Théorie de la démonstration, Cours et exercices corrigés with René David et Karim Nour, Dunod (2001).
Simple proof of the completeness theorem for second order classical and intuitionistic logic, with Karim Nour, TCS, Volume 308, Issues 1-3 , 3 November 2003, Pages 227-237. Download pdf.
An optimized complete semi-algorithm for system F-eta (1999). Download pdf.
Completeness, minimal logic and programs extraction, Theoretical Computer Science, Vol. 254, p259-271 (2001). Download pdf.
System F-eta, prépublication 98-05a du LAMA (1998). Download pdf.
A semantical storage operator theorem for all types, Annals of Pure and Applied Logic, Vol. 91, p17-31 (1998). Download pdf.
L'Arithmétiques Fonctionnelle du Second Ordre avec Points Fixes, Thèse de l'université Paris VII (1994). Download pdf.
Data Types, Infinity and Equality in System AF2 Computer Science Logic, Lecture Notes in Computer Science, Vol. 832, p280-294 (1993). Download pdf.
Machine Deduction, Types for Proofs and Programs, Lecture Notes in Computer Science, Vol. 806, p333-351 (1993). Download pdf.