RAFFALLI CHRISTOPHE

Les démonstrations mathématiques, Ellipses Introduction à la logique, Dunod

Articles in journal and proceedings, prepuplications

(below you will find some selected talks)
[Raf23]
Isotopic piecewise affine approximation of algebraic varieties (2023). Prepublication on ArXiv (download pdf)
[Raf22]
On a question of supports, with Frédéric Mangolte (2022). European Journal of Mathematics, Volume 8, Issue 3, pages 1036-1041. Download pdf.
[Raf20]
Computational contents of classical logic and extensional choice to be submitted soon. pdf
[Raf19]
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.
[Raf18]
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.
[Raf17]
Les démonstrations mathématiques with René David, Pierre Hyvernat and Karim Nour, Ellipses, 2017, ISBN : 9782340016668.
[Raf14a]
Mêler combinateurs, continuations et EBNF pour une analyse syntaxique efficace en OCaml avec Rodolphe Lepigre, 2014 available in pdf
[Raf13c]
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
[Raf13b]
Distance to the discriminant. in preparation, pdf.
[Raf13a]
Nullstellensatz and positivestellensatz from cut-elimination (draft available in pdf or ps is you have problem to print the pdf).
[Raf10c]
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.
[Raf10b]
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.
[Raf10a]
MathNat - Mathematical Text in a Controlled Natural Language with Muhammad Humayoun, available in pdf (proceedings of Cicling 2010, Roumania)
[Raf06a]
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
[Raf05a]
PhoX with Paul Rozière in The seventeen provers of the World Freek Wiedijk (editor) LNAI 3600 pages 67-71.
[Raf03b]
System ST Schedae Informatica, proceedings of the Chambery-Krawow-Lyon Workshop, Vol. 12, pages 97-112 (June 2003)
[Raf03a]
GlSurf, Maths et Dessins en OCaml, (2003). JFLA 2004. Download: pdf or ps.
[Raf02c]
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 or ps.
[Raf02b]
Système St, beta-reduction and completeness, presented at LICS 2003, publication IEEE, pages 21-32. Formal proofs in PhoX available. Download pdf or ps.
[Raf02a]
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 or ps.
[Raf01d]
Système 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 or ps.
[Raf01c]
Apprentissage du raisonnement assité par ordinateur, avec René David, Quadrature numéro 45, printemps 2002, pages 25-36). Downloaad pdf or ps.

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

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

Last update: Friday 7 April 2023