Diss.--Mathematik--München--Ludwig-Maximilians Universität, 2001. / Notes bibliogr. Bibliogr. 1 p. Index.

La thèse décrit un lambda calcul typé étendu par un traitement des exceptions. Ses principales propriétés sont : confluence, forte normalisation, conservation du type (dans une forme parallélisée de réduction). Seuls les termes équivalents aux entiers de Church ont le type entier. La comparaison avec le système d'exceptions du langage Caml est développée. Mais le plus remarquable est que la logique du système n'est pas la logique classique mais la logique intuitionniste.

Cette thèse s'intéresse à l'usage des formalismes d'inférence profonde comme fondement des interprétations calculatoires des systèmes de preuve, en suivant les deux approches principales: celle des preuves comme programmes et celle de la recherche de preuve comme calcul. La première contribution est le développement d'une famille de systèmes de preuve pour la logique intuitionniste dans le calcul des structures et dans les séquents imbriqués. pour lesquels des procédures de normalisation internes sont fournies. L'une de ces procédures est alors interprétée en termes calculatoires, comme un raffinement de la correspondance de Curry-Howard permettant d'introduire une forme de partage ainsi que des opérateurs de communication dans un lambda-calcul avec substitution explicite. Du coté de la recherche de preuve, la notion de preuve focalisée en logique linéaire est transférée du calcul des séquents au calcul des structures, où elle induit une forme incrémentale de focalisation, dotée d'une preuve de complétude très simple. Enfin, une autre interprétation de la recherche de preuve est donnée par l'encodage de la réduction d'un lambda-calcul avec substitution explicite dans les règles d'inférence d'un sous-système de la logique intuitionniste dans le calcul des structures.

Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.