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. / Proving program equivalence for a functional language with references is a notoriously difficult problem. The goal of this thesis is to propose a logical system in which such proofs can be formalized, and in some cases inferred automatically. In the first part, a generic extension method of dependent type theory is proposed, based on a forcing interpretation seen as a presheaf translation of type theory. This extension equips type theory with guarded recursive constructions, which are subsequently used to reason on higher-order references. In the second part, we define a nominal game semantics for a language with higher-order references. It marries the categorical structure of game semantics with a trace representation of denotations of programs, which can be computed operationally and thus have good modularity properties. Using this semantics, we can prove the completeness of Kripke logical relations defined in a direct way, using guarded recursive types, without using biorthogonality. Such a direct definition requires omniscient worlds and a fine control of disclosed locations. Finally, we introduce a temporal logic which gives a framework to define these Kripke logical relations. The problem of contextual equivalence is then reduced to the satisfiability of an automatically generated formula defined in this logic, i.e. to the existence of a world validating this formula. Under some conditions, this satisfiability can be decided using a SMT solver. Completeness of our methods opens the possibility of getting decidability results of contextual equivalence for some fragments of the language, by giving an algorithm to build such worlds.
| Identifer | oai:union.ndltd.org:theses.fr/2014EMNA0124 |
| Date | 11 July 2014 |
| Creators | Jaber, Guilhem |
| Contributors | Nantes, Ecole des Mines, Miquel, Alexandre |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0572 seconds