Logique, Réalisabilité et Concurrence

Overview & Synopsis

Cette thèse se consacre à l'application de techniques de réalisabilité dans le cadre de l'étude du sens calculatoire de la logique. Dans une première partie, nous rappelons le formalisme de la réalisabilité classique de Krivine, dans lequel nous menons ensuite une étude du contenu opérationnel de tautologies purement classiques. Cette exploration du sens calculatoire de la disjonction classique révèle des comportements riches, avec une forte intuition interactive, qui s'interprètent avantageusement comme des structures de contrôle typées. Afin de mieux comprendre la nature de ces mécanismes, nous définissons ensuite une technique de réalisabilité à la Krivine pour un modèle de calcul concurrent, dans le but d'obtenir une notion de constructivité qui ne soit plus fondée sur l'idée de fonction, mais sur celle de processus interactif. Le cadre ainsi obtenu donne une interprétation réellement concurrente de la logique linéaire dans un calcul de processus dérivé du pi-calcul, permettant d'appliquer au cas concurrent la méthode de spécification précédemment étudiée dans le cas séquentiel. Par la suite, l'étude des traductions de la logique classique vers la logique linéaire mène à reconstruire systématiquement des décompositions interactives du calcul fonctionnel, permettant ainsi de faire le lien au niveau logique entre les réalisabilités classique et concurrente. Dans une dernière partie, nous étudions plus en détail le mode de calcul issu des algèbres de processus, afin de comprendre son système d'ordonnancement. Cette étude mène à la définition d'un modèle de calcul plus géométrique qui permet une exploration formelle de la notion de causalité dans les calculs concurrents.