Soutenance de la thèse de Benjamin Leperchey

Ma soutenance aura lieu

Jury

Sur la notion d'observation en sémantique

Cette thèse explore plusieurs aspects de la notion d'observation en sémantique des langages de programmation fonctionnels. Après avoir rappelé les notions de base sur PCF et ses variantes finitaires, nous présentons les notions d'observation syntaxique et d'observation dénotationnelle, ainsi que les relations logiques, qui sont le principal outil pour étudier les modéles des langages fonctionnels.

Nous étudions d'abord les degrés de définissabilité relative. Nous prouvons que, dans le cas de PCF unaire, il n'existe que deux modèles standard extensionnels pour l'ordre, alors qu'il existe au moins quatre degrés de définissabilité distincts dans le modèle de Scott. Nous nous penchons ensuite sur la définissabilité relative au premier ordre dans le modèle de Scott de PCF finitaire, en approfondissant les travaux de Bucciarelli et Malacaria sur les hypergraphes colorés. Grâce à la notion d'hypergraphe temporisé, nous présentons une carctérisation de la définissabilité relative en termes géométrique complète pour les fonctions sous-séquentielles. Enfin, nous analysons les travaux de Longley sur le modèle des fonctions séquentiellement réalisables (isomorphe au modèles des fonctions fortement stables), et proposons une interprétation de sa fonctionnelle H à l'aide d'une traduction en Caml.

Nous nous attaquons ensuite à un langage avec des références allouées sur le tas où, à la différence de ML il n'est pas possible d'enregistrer des fonctions mais seulement des entiers ou d'autres références. Nous présentons un modèle dénotationnel construit à l'aide de la théorie Fränkel-Mostowski, qui offre un cadre élégant pour traduire l'allocation dynamique. Pour remédier à des problèmes d'incomplétude, nous introduisons des relations paramétrique à la Pitts et Stark ou Reddy et Yang, qui utilisent la notion originale de fonction d'accessibilité, qui repréente la patrie du tas accessible par un terme. Pour évaluer la qualité du modèle obtenu, nous le confrontons à une suite d'exemples classiques (la suite de Meyer-Sieber) et originaux. Il reste à résoudre le problème du snapback, qui brise certaines égalités dans le modèle. Nous terminons par une ouverture vers des problématiques de sécurité, en appliquant ces techniques à l'étude de protocoles cryptographiques.

Dans une troisième partie, nous présentons une construction catégorique pour représenter le temps de calcul dans un modèle dénotationnel traditionnel. Nous montrons que, sous quelques hypothèses simples (l'existence d'une monade et d'un morphisme tick), on peut construire un modèle correct et adéquat d'une version temporisée de PCF. Nous appliquons cette technique au modèle des espaces de cohérence et au modèle de jeux de Hyland et Ong. Ce dernier modèle est complètement adéquat pour le notion d'observation qui prend en compte la longueur du calcul. Nous présentons enfin quelques idées sur l'utilisation de la longueur des partie de la sémantique des jeux pour représenter un temps de calcul, avec une nouvelle classe de stratégies, les stratégies semi-alternantes.

On the notion of observation in semantics

This thesis explores several aspects about the notion of observation in semantics of functional programming languages. After recalling the basics about PCF and its finitary versions, we present the notions of syntactical and denotational observation, and the logical relations, which are the main tool for studying the models of functional programing languages.

We first investigate degrees of relative definability. We show that, in the case of unary PCF, there are only two standard ordre extensional models, although at least four distinct degrees of definability can be found in the Scott model. We then turn to finitary PCF, and refine the notion of colored hypergraph of Bucciarelli and Malacaria. Thanks to the notion of timed morphisms, we are able to give a geometrical characterization of relative definability at first orderin the Scott model, which is complete for subsequential functions. Finally, we analyze the work of Longley on the sequentially realizable functionals model (which is isomorphic to the strongly stable model), and give an interpretation of the H functional through its Caml implementation.

We then study a language with heap-allocated references where, unlike in ML, one cannot store functions but only integers and other references. We present a denotational model based on the permutation theory of Fraenkel and Mostowksi, which allows an elegant translation of the dynamic allocation. To address completeness issues, we instrument the model with parametric logical relations, in the style of Pitts and Stark, and Reddy and Yand, which use the original notion of accessibility map, an abstract representation for the part of the heap accessible by a term. To evaluate the model, we test it against several test cases. It passes all the Meyer-Sieber suite, but fails on the snapback example. We finally give some hints on how to apply these techniques to security issues, with an example about cryptographic protocols.

In the last part of the thesis, we present a categorical way of enriching a standard model to represent the length of computation. We show that, under reasonable assumptions (exsitence of a monad and a tick morphism), one can build a sound and adequate model of a timed version of PCF. We apply this technique to the coherence model and the games of Hyland and Ong. The latter is shown to be fully abstract for the notion of improvement. We finally give some ideas on using the length of the sequences of moves of the game semantics to represent the length of computation, and present the original notion of semi-alternating strategies.