Articles de recherche
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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 ».
-
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.
-
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.
-
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 »).
-
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.
-
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.
-
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.
-
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é.
-
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.
-
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.
-
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
« 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
-
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é.
-
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.
-
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
-
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).