Articles

2024, 2023, 2021, 2020, 2018, 2016, 2014, 2012, 2011, 2010, 2009, 2008, 2007, 2005, 2004, 2003, 2001, 2000, 1990's, 1980's, thèse et mémoires, divers
2024
« An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem » (version étendue de janvier 2024, soumise) (version de 2016) (version de novembre 2022, incluant la disjonction), (programme OCaml correspondant), en collaboration avec Danko Ilik.
2023
« A parametricity-based formalization of semi-simplicial and semi-cubical sets », en collaboration avec Ramkumar Ramachandra, mise à jour de décembre 2023, soumis (la formalisation en Coq).
2021
« On the logical structure of choice and bar induction principles », en collaboration avec Nuria Brede, paru dans les actes de LICS '21 (bibtex) (résumé illustré) (errata, pdf avec errata inclus) (formalisation en Coq par Étienne Miquey, jusqu'aux Théorème 2 et Proposition 8).
2020
« A calculus of expandable stores », en collaboration avec Étienne Miquey, paru dans les actes de LICS '20 © IEEE (bibtex).
2018
« Realizability interpretation and normalization of typed call-by-need lambda-calculus with control », en collaboration avec Étienne Miquey, paru dans les actes de FoSSaCS '18 (bibtex).
2016
« An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem », en collaboration avec Danko Ilik.
2014
« A dependently-typed construction of semi-simplicial types », Mathematical Structures in Computer Science, 2015 (erratum) (bibtex) (la formalisation en Coq).
2012
« A constructive proof of the axiom of dependent choice, compatible with classical logic », paru dans les actes de LICS '12 © IEEE (erratum, pdf avec erratum inclus) (bibtex) (exposé LICS '12) (la preuve en Coq).
Résumé: En restreignant la règle d'élimination forte de l'existentielle (= règle d'élimination de la somme dépendante de Martin-Löf) à la classe des preuves n'utilisant pas de règles d'élimination de connecteurs négatifs, nous obtenons une logique constructive qui prouve l'axiome du choix dépendant tout en restant compatible avec la logique classique.
« Classical call-by-need sequent calculi: The unity of semantic artifacts », en collaboration avec Zena Ariola, Paul Downen, Keiko Nakata et Alexis Saurin, paru dans les actes de FLOPS '12 © Springer-Verlag (bibtex).
2011
« Pure Type Systems conversion is always typable », en collaboration avec Vincent Siles, paru dans le Journal of Functional Programming, 2011 (bibtex).
« Classical Call-by-Need and Duality », en collaboration avec Zena Ariola et Alexis Saurin, paru dans les actes de TLCA '11 (bibtex).
2010
« An intuitionistic logic that proves Markov's principle », paru dans les actes de LICS '10 © IEEE (typos) (bibtex) (exposé LICS '10).
« Equality is typable in Semi-Full Pure Type Systems », en collaboration avec Vincent Siles, paru dans les actes de LICS '10 © IEEE (bibtex).
« Kripke models for Classical Logic », en collaboration avec Danko Ilik et Gyesik Lee, paru dans le numéro spécial « Classical Logic and Computation », Annals of Pure and Applied Logic, 2010 (bibtex).
« λ-calculus and Λ-calculus: a Capital Difference », en collaboration avec Alexis Saurin, manuscrit, 2010.
2009
« An operational account of call-by-value minimal and classical lambda-calculus in "natural deduction" form », en collaboration avec Stéphane Zimmermann, paru dans les actes de TLCA '09, LNCS 5608 © Springer-Verlag (errata inclus) (bibtex).
Résumé: Cet article s'inspire de la simplicité de la théorie de l'appel par valeur dans le calcul des séquents pour analyser la théorie de l'appel par valeur dans le cadre plus standard du lambda-calcul, avec ou sans contrôle. Les principaux résultats sont:
- une description inédite de la théorie équationnelle du lambda-calcul avec contrôle sous la forme d'un système de réécriture confluent,
- la différentiation entre les notions de régles de réduction opérationnelles, qui sont nécessaires à l'évaluation des termes clos, de régles de réduction structurelles, qui sont nécessaires pour révéler des rédex opérationnels dans les termes non clos, et de régles de réduction observationnelles, qui ne sont nécessaires que pour des raisons de complétude sémantique (par exemple vis à vis de la sémantique par passage de continuation)
- une tentative de reformulation de la notion de standardisation en appel par valeur qui répare quelques défauts de la définition originelle de Plotkin.
A posteriori, il n'est pas clair que la notion de règles structurelles soit intéressante et il serait sans doute préférable de considérer ces règles  structurelles  comme opérationnelles pour un certain critère d'arbre de Böhm pour l'appel par valeur. Il n'est pas clair non plus que la reformulation donnée de la standardisation soit la bonne : là aussi, il aurait sans doute été préférable de considérer les règles structurelles comme opérationnelles.
« Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus », avec Gyesik Lee, paru dans les actes de WOLLIC '09 (bibtex).
2008
« A new elimination rule for the Calculus of Inductive Constructions », en collaboration avec Bruno Barras, Pierre Corbineau, Benjamin Grégoire et Jorge Luis Sacchini, paru dans « TYPES '08, selected papers », LNCS 5497 (bibtex).
« An approach to call-by-name delimited continuations », en collaboration avec Silvia Ghilezan, paru dans les actes de POPL '08 (© ACM - avec la permission de ACM - ne pas redistribuer) (errata) (bibtex) (exposé POPL '08).
Résumé : Saurin a montré que la variante de de Groote du lambda-mu-calcul de Parigot était strictement plus expressive dans le cas non typé que le calcul original de Parigot. On montre ici que ce surcroît d'expressivité correspond exactement à l'ajout de continuations délimitées de telle sorte que le calcul de de Groote peut être interprété comme l'exact pendant en appel par nom du calcul shift-reset de Danvy et Filinski. Cette « dualité » est exprimée dans le cadre d'un lambda-mu-calcul étendu avec une variable de continuation représentant le toplevel et liée dynamiquement : le calcul lambda-mu-tp-hat. Une correspondance équationnelle entre la version appel par valeur de ce calcul et le calcul de Danvy et Filinski ayant déjà été montrée dans A type-theoretic foundation of delimited continuations, on se contente de montrer ici l'équivalence entre la version appel par nom et le calcul de de Groote. On réalise en passant une étude comparée des sémantiques opérationnelles, des transformations par passage de continuations, et du typage simple des versions appel par nom et appel par valeur du calcul lambda-mu-tp-hat. On conclut en montrant l'existence de deux autres calculs canoniques de continuations délimitées, l'un d'entre eux étant le calcul shift/lazy-reset de Sabry et l'autre une version « paresseuse » du calcul de de Groote.
2007
« Control Reduction Theories: the Benefit of Structural Substitution », en collaboration avec Zena Ariola, Journal of Functional Programming, 2007 (bibtex).
Résumé : On donne une analyse fine des différences entre le lambda-C-calcul de Felleisen et al. et le lambda-mu-calcul de Parigot (présenté, pour faciliter la comparaison, avec un opérateur C et, pour le besoin d'expressivité, avec une continuation « toplevel »), les deux calculs étant considérés dans leur variante appel par valeur et non typée. On montre que la substitution structurelle des contextes d'évaluation propre au lambda-mu-calcul débouche sur une théorie bien plus riche et harmonieuse que celle du lambda-C-calcul de Felleisen et al. Malgré tout, les deux calculs restent observationnellement équivalents.
« A Type-Theoretic Foundation of Delimited Continuations », en collaboration avec Zena Ariola et Amr Sabry, Higher-Order and Symbolic Computation, 2007 © Springer-Verlag (bibtex).
Cet article est une version longue et sensiblement améliorée de « A Type-Theoretic Foundation of Continuations and Prompts ».
2005
« On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic », paru dans les actes de TLCA '05, LNCS 3461 (erratum) (bibtex) © Springer-Verlag (la preuve de dégénérescence typée en Coq ancienne syntaxe).
Résumé : On considère une théorie de Sigma-types (autrement dit une théorie des types restreinte à l'existentielle forte -- parfois aussi appelée somme forte). On montre que le domaine de quantification des types Sigma est dégénéré (c'est-à-dire prouvablement réduit à au plus un seul élément) en présence de logique classique calculatoire, c'est-à-dire en présence d'un opérateur de type callcc équipé de règles de réduction standard. On montre toutefois que la non dégénérence n'est pas dérivable si l'opérateur classique est typé et que la règle d'éta-réduction propre à cet opérateur (i.e. « callcck M -> M, pour k ne figurant pas dans M ») est supprimée.
« Type inference with algebraic universes in the Calculus of Inductive Constructions », manuscrit, 2005.
2004
Résumé : Cet article étudie le lambda-mu-calcul de Parigot en appel par valeur étendu avec une variable de continuation liée dynamiquement (de plus le mu est representé avec le C de Felleisen). On montre notamment que ce calcul est équivalent au calcul shift-reset de Danvy-Filinski. La correspondance est obtenue en décomposant la double transformation par passage de continuation qui définit shift-reset en une transformation par passage d'état suivie d'une transformation simple par passage de continuation. Plusieurs systèmes de types sont étudiés et on montre qu'ils garantissent la normalisation forte du calcul à partir du moment où, soit on ajoute des effets aux types, soit on se restreint à n'appeler reset que sur des types atomiques. L'article insiste aussi sur le rôle du connecteur soustraction pour simuler de manière purement fonctionnelle l'aspect dynamique d'une variable de continuation telle que celle utilisée pour interpréter l'opérateur reset. Accessoirement, on trouve dans la version longue une preuve détaillée de normalisation forte de la déduction naturelle classique étendue avec le connecteur soustraction. Notons aussi que la version longue corrige l'énoncé de la proposition 8 qui est incorrect tel que donné dans la version conférence.
2003
« Minimal classical logic and control operators », en collaboration avec Zena Ariola, paru dans les actes de ICALP '03 - LNCS 2719 © Springer-Verlag (erratum) (bibtex) (exposé au format Active dvi ou pdf). Une version « journal » avec Amr Sabry est parue dans Higher-Order and Symbolic Computation sous le titre « A Proof-Theoretic Foundation of Abortive Continuations ».
Résumé : La logique classique minimale est définie comme la restriction de la logique classique qui vérifie la loi de Peirce mais pas l'axiome «  ex falso quodlibet  » (et donc pas l'élimination de la double négation). En particulier, le lambda-mu-calcul de Parigot dénote les preuves de la déduction naturelle classique minimale. Pour obtenir la logique classique complète, il faut étendre le lambda-mu-calcul avec une constante de type l'absurde qui s'interprète calculatoirement comme la continuation « toplevel ». Enfin, on présente un raffinement de l'opérateur C de Felleisen et al. qui permet une correspondance étroite avec le lambda-mu-calcul et qui a de « bonnes propriétés ».
2001
« Explicit Substitutions and Reducibility », Journal of Logic and Computation, Vol 11(3), pp 429-449, 2001 © Oxford University Press (la preuve du lemme d'affaiblissement y est incorrecte... des détails) (bibtex).
Mots-clés : Lambda-bar-calcul, Substitutions explicites, Normalisation forte, Réductibilité
Résumé : On définit une notion de réductibilité basée sur les séquents et non sur les formules. On en tire une preuve directe de normalisation forte pour le lambda-bar-calcul avec substitution explicite.
2000
« The duality of computation », en collaboration avec Pierre-Louis Curien (Proceedings of ICFP '00 © ACM) (errata, version ps avec errata inclus, pdf) (bibtex). L'exposé plus récent à WoLP '04 au format advi (installer Active dvi) ou ps. Les notes de l'exposé invité à HOR '06 (bibtex).
Mots-clés : Appel par valeur, Appel par nom, Calcul des Séquents, Traductions CPS, Correspondance preuve-programme de Curry-Howard-de Bruijn, Dualité, Lambda-Calcul
Résumé : On montre que la symétrie gauche-droite du calcul des séquents de Gentzen exprime une dualité entre termes et contextes et entre appel par nom et appel par valeur; on développe le lambda-bar-calcul, une variante du lambda-calcul qui rend explicite ces dualités.
1998
« Computing with Abstract Böhm Trees », conjointement avec Pierre-Louis Curien, paru dans les actes de FLOPS'98 (bibtex).
Mots-clés : Modèles du calcul en termes de jeux, Machines abstraites, Arbres de Böhm.
Résumé : On présente et compare plusieurs variantes de machines abstraites pour la réduction faible de tête en lambda-calcul, en PCF, et, plus généralement, dans un langage abstrait d'arbres de Böhm. Certaines de ces machines sont exprimées dans un formalisme de la théorie des jeux (telle la « machine abstraite géométrique » qui est originale). Les autres sont exprimées sous la forme de banales machines à environnement du type KAM (on notera en particulier une « machine abstraite de Krivine sans pile  »).
1997
« Games and weak-head reduction for Classical PCF », paru dans les actes de TLCA'97 , LNCS 1210 (bibtex).
Mots-clés : Modèles du calcul et de la prouvabilité en termes de jeux, Machines abstraites, Logique classique, Opérateurs de contrôle, Lambda-mu-calcul.
Résumé : On montre une extension du modèle de Hyland et Ong au cas de PCF avec catch et throw. L'interprétation diffère de celle de Ong en ce qu'elle restreint les règles de jeux tandis que Ong étend les coups possibles. On montre au passage les rapports entre les E-dialogues de Lorenzen, le débat de Coquand, la machine de Krivine, le lambda-mu-calculus de Parigot et le modèle en termes de jeux.
1996
« Game semantics and abstract machines », conjointement avec Vincent Danos et Laurent Regnier, Proceeding of LICS'96 (bibtex).
Mots-clés : Machines abstraites, Modèles du calcul en termes de jeux (Hyland-Ong, Abramsky-Jagadeesan-Malacaria), Géométrie de l'interaction.
Résumé : On montre que la composition dans le modèle en termes de jeux de Hyland et Ong pour PCF correspond à la réduction linéaire de tête dans une machine abstraite en appel par nom. On montre aussi que la composition dans le modèle de Abramsky-Jagadeesan-Malacaria est lié à la géométri de l'interaction.
« Une caractérisation des stratégies indépendantes de l'histoire à partir des stratégies innocentes », manuscrit, 1996.
Mots-clés : Modèles du calcul en termes de jeux (Hyland-Ong, Abramsky-Kagadeesan-Malacaria).
Résumé : On caractérise les stratégies du modèle de Abramsky-Kagadeesan-Malacaria en termes de stratégies du modèle de Hyland-Ong.
1995
« Notes sur les lambda-sigma-calculs », manuscrit, 1995.
Mots-clés : Lambda-calculs avec substitutions explicites, Confluence, Non terminaison forte.
Résumé : On montre qu'une version simple de lambda-calculs avec substitution explicite, sans composition mais avec règle Map, suffit à faire perdre la normalisation forte dans le cas simplement typé.
1994
« A lambda-calculus structure isomorphic to sequent calculus structure », Proceedings of CSL'94 (bibtex).
« A lambda-calculus structure isomorphic to sequent calculus structure », version étendue au calcul des prédicats, manuscrit, 1994 .
Mots-clés : Calcul des séquents, Analogie preuve/programme (correspondance de Curry-Howard), Lambda-calculs avec substitution explicite.
Résumé : On étend l'analogie preuve/programme en exhibant un lambda-calcul avec substitution explicite interprétant les preuves du calcul des séquents de Gentzen.
« A-translation and looping combinators in Pure Type Systems », conjointement avec Thierry Coquand, Journal of Functional Programming , Volume 4, 1994 (bibtex).
Mots-clés : Systèmes de types, Complétude de Turing, Systèmes logiques incohérents.
Résumé : On montre que dans les théories des types (Théorie des types de Martin-Löf, Calcul des Constructions, ...), on peut encoder toutes les fonctions partielles récursives dès que la théorie est logiquement incohérente (ce qui est le cas des systèmes Type:Type de Martin-Löf, et U de Girard,...). La méthode employée repose sur la A-traduction de Friedman. Une conséquence est aussi l'indécidabilité de la vérification de type dans Type:Type.
« Some remarks on Novikoff's calculus », avec Thierry Coquand, manuscrit, 1994.
Mots-clés : Logique classique, Elimination des coupures, Extraction de programmes.
Résumé : Une solution au problème soulevé dans mon mémoire de magistère
1993
« Weak reduction in sequent calculus », manuscrit, 1993, intégré en français dans le chapitre 6 de ma thèse.

« Weak cut-elimination and the game-theoretic approach of provability », manuscrit (11 pages), 1993, intégré en français dans le chapitre 6 de ma thèse.

1989
« The two-list algorithm for the knapsack problem on a FPS T20 », conjointement avec Afonso Ferreira et Michel Cosnard, short communication, Parallel Computing , Volume 9, North Holland, 1989 (seule la version papier est disponible).

Thèse et mémoires

HdR
« C'est maintenant qu'on calcule: au cœur de la dualité », mémoire d'habilitation, 2005. Cf page spécifique.
Thèse
« Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes », thèse de doctorat, 1995 (errata) (bibtex).
Mots-clés : Calcul des séquents, Elimination des coupures, Lambda-calculs, Modèles de la prouvabilité en terme de jeux (Lorenzen, Coquand), Logique classique.
Résumé :
  • On interprète le calcul des séquents de Gentzen comme un lambda-calcul (extension de l'isomorphisme de Curry-Howard au calcul des séquents).
  • On montre que les jeux de Lorenzen ne sont rien d'autres qu'une paraphrase de la prouvabilité dans un certain calcul des séquents.
  • On montre que l'élimination des coupures dans le modèle en terme de jeux de Coquand correspond à l'élimination faible de tête des coupures dans le calcul des séquents modélisé.
Mag.
« Extraction de programmes à partir de preuves de la logique classique » , mémoire de magistère, 1991.
Mots-clés : Logique classique, Extraction de programmes.
Résumé : On décrit un exemple de preuve en logique classique pour lequel les méthodes d'extraction automatique de programme ne fournisse pas un résultat satisfaisant.
DEA
Mots-clés : Preuve formelle sur machine, Théorie stratifiée des ensembles.
Résumé : On formalise le théorème de Schröder-Bernstein dans le système Coq de l'INRIA.

Articles de dissémination

« Coq, assistant de preuve », avec Sandrine Blazy et Pierre Castéran, Techniques de l'ingénieur, 2017

« TYPES: Types for Proofs and Programs », rapport synthétique sur le projet européen BRA-TYPES, Bulletin of the European Association on Theoretical Computer Science , octobre 1994.

Mots-clés : Systèmes d'aide à la preuve, Théories des types, Actions européennes de recherche.

Résumé : On fait une synthèse des efforts d'implémentation et de recherche effectués dans le cadre de l'action européenne BRA-TYPES.

Sous-produits de mon enseignement

Projets de programmation fonctionnelle
« Compilation de Mini-Scheme/Mini-ML en instructions pour une machine à environnement », distribué avec une implémentation en Caml-Light.
L'énoncé
Une implémentation complète en Caml-Light (archive compressée « .tar.gz »)

« Interpréteur de lambda-calcul pur »
L'énoncé
Une implémentation complète en Caml-Light (archive compressée « .tar.gz »)

Projets d'architecture
« Simulation du micro-processeur micro-programmé de l'ouvrage d'architecture de Tanenbaum »
Les sources pour DCS (Design Capture System) (archive compressée « .tar.gz » 1.8M)
Mémoire d'enseignement
« Difficultés conceptuelles dans l'enseignement du C », mémoire d'enseignement, CIES de Lyon (2 pages).