Accueil > Manifestations > Thèses et HDR > Thèses > Guilhem Jaber

Guilhem Jaber

Directeur de thèse

Alexandre Miquel
Nicolas Tabareau

Résumé

Prouver l’équivalence de programmes écrits dans un langage fonctionnel avec références est un problème notoirement difficile. L’objectif de cette thèse est de proposer un système logique dans lequel de telles preuves peuvent être formalisées, et dans certains cas inférées automatiquement.

Dans la première partie, une méthode générique d’extension de la théorie des types dépendants est proposée, basée sur une interprétation du forcing vu comme une traduction de préfaisceaux de la théorie des types. Cette extension dote la théorie des types de constructions récursives gardées, qui sont utilisées ensuite pour raisonner sur les références d’ordre supérieure.

Dans une deuxième partie, nous définissons une sémantique des jeux nominale opérationnelle pour un langage avec références d’ordre supérieur. Elle marie la structure catégorique de la sémantique des jeux avec une représentation sous forme de traces de la dénotation des programmes, qui se calcule de manière opérationnelle et dispose donc de bonnes propriétés de modularité.

Cette sémantique nous permet ensuite de prouver la complétude de relations logiques à la Kripke définit de manière directe, via l’utilisation de types récursifs gardés, sans utilisation de la biorthogonalité. Une telle définition directe nécessite l’utilisation de mondes omniscient et un contrôle fin des locations divulguées.

Finalement, nous introduisons une logique temporelle qui donne un cadre pour définir ces relations logiques à la Kripke.
Nous ramenons alors le problème de l’équivalence contextuelle à la satisfiabilité d’une formule de cette logique générée automatique,
c’est à dire à l’existence d’un monde validant cette formule. Sous certaines conditions, cette satisfiabilité peut être décidée via l’utilisation d’un solveur SMT.
La complétude de notre méthode devrait permettre d’obtenir des résultats de décidabilité pour l’équivalence contextuelle de certains fragment du langage considéré, en fournissant un algorithme pour construire de tels mondes.

Mots-clés : Théorie des Types, Forcing, Equivalence Contextuelle, Relation Logique, Sémantique des Jeux, Logique Temporelle.

Composition du jury :

  • Lars Birkedal, Professor, Aarhus University, Rapporteur
  • Martin Hofmann, Professor, LMU München, Rapporteur
  • Nick Benton, Senior Researcher, Microsoft Research Cambridge, Examinateur
  • Pierre Cointe, Professeur, École des Mines de Nantes, Examinateur
  • Pierre-Louis Curien, Directeur de Recherche CNRS PPS, Université Paris 7, Examinateur
  • Alexandre Miquel, Professeur, Universidad de la República - Montevideo, Directeur de thèse
  • Nicolas Tabareau, Chargé de Recherche, Inria Rennes-Bretagne-Atlantique, co-encadrant de thèse

Dernière modification : vendredi 4 juillet 2014