Ma thèse s'intitule Semantics of linear logic and higher-order model-checking, qui se traduit donc Sémantique de la logique linéaire et model-checking d'ordre supérieur. Le manuscrit, rédigé en anglais, est disponible ici. Ce n'est pas la version définitive : quelques corrections mineures vont être apportées. N'hésitez pas à m'envoyer tout commentaire à son sujet. Le résumé en français est disponible ici.



My thesis is entitled Semantics of linear logic and higher-order model-checking. The manuscript is available here. Some minor corrections are still to be done. Please send me any comment you have about it. The abstract is available here.



Le jury sera composé de:

  • Ugo Dal Lago, Université de Bologne & INRIA, Examinateur
  • Thomas Ehrhard, CNRS & Université Paris Diderot - Paris 7, Président du jury
  • Jean Goubault-Larrecq, CNRS & ENS Cachan, Examinateur
  • Paul-André Melliès, CNRS & Université Paris Diderot - Paris 7, Directeur de thèse
  • Luke Ong, Merton College, University of Oxford, Examinateur
  • Olivier Serre, CNRS & Université Paris Diderot - Paris 7, Co-directeur de thèse
  • Kazushige Terui, Research Institute for Mathematical Sciences, Kyoto University, Rapporteur
  • Igor Walukiewicz, CNRS & Université de Bordeaux, Rapporteur



La soutenance de ma thèse aura lieu vendredi 8 avril 2016, à 10h, en salle 2011 du bâtiment Sophie Germain. La soutenance sera suivie d'un pot au 3e étage, sur le plateau central de l'équipe PPS. Un plan d'accès au bâtiment Sophie Germain suit. Attention, pour des raisons de sécurité, je dois communiquer le nom de tous les extérieurs venant assister à la soutenance: merci de m'envoyer un mail si vous comptez venir, sans quoi vous ne pourrez pas rentrer.

Pour l'accès en transports en commun, vous pouvez notamment utiliser le RER C ou le métro 14 jusqu'à Bibliothèque François Mitterrand, ou le tramway 3a jusqu'à l'arrêt Porte de France. Certains bus passent aussi, dont le 89.



My PhD thesis defense will take place on Friday, April 8, 2016 at 10am, in the Sophie Germain building, room 2011. There will be a small reception afterwards, on the 3rd floor, which hosts the PPS team. An access map to the Sophie Germain building follows. Beware, for security reasons, I need to provide a list of all the people who intend to come. Please send me an email if you do, else you may not be able to enter the building.

To come using public transportation, you can notably use RER C or metro 14 to Bibliothèque François Mitterrand. Tramway 3a to the stop "Porte de France" is another option. Some buses, among which the 89, may also be convenient.





Le bâtiment Sophie Germain est en arrière-plan:

The Sophie Germain building is the one in the background:



This thesis studies problems of higher-order model-checking from a semantic and logical perspective. Higher-order model-checking is concerned with the verification of properties expressed in monadic second-order logic, specified over infinite trees generated by a class of rewriting systems called higher-order recursion schemes. These systems are equivalent to simply-typed λ-terms with recursion, and can therefore be studied using semantic methods.

The more specific purpose of this thesis is to connect higher-order model-checking to a series of advanced ideas in contemporary semantics, such as linear logic and its relational semantics, indexed linear logic, distributive laws between comonads, parametric comonads and tensorial logic. As we will see, all these ingredients meet and combine surprisingly well with higher-order model-checking.

The starting point of our approach is the study of the intersection type system of Kobayashi and Ong. This intersection type system enables one to type a higher-order recursion scheme with states of a given automaton, associated with a formula of monadic second-order logic. The recursion scheme is typable with the initial state of the automaton if and only if the infinite tree it represents satisfies the formula of interest. In spite of this soundness-and-completeness result, the original type system by Kobayashi and Ong was not designed with the connection between intersection types and models of linear logic observed by Bucciarelli, Ehrhard, de Carvalho and Terui in mind. Our work has thus been to connect these two fields.

Our analysis leads us to the definition of an alternative intersection type system, which enjoys a similar soundness-and-completeness theorem with respect to higher-order model-checking. In contrast to the original type system by Kobayashi and Ong, our modal formulation is the proof-theoretic counterpart of a finitary semantics of linear logic, obtained by composing the traditional exponential modality with a coloring comonad. We equip the semantics of linear logic with an inductive-coinductive fixpoint operator. We obtain in this way a model of the λ-calculus with recursion in which the interpretation of a higher-order recursion scheme is the set of states from which the infinite tree it represents is accepted. The finiteness of the semantics enables us to reestablish several results of decidability for higher-order model-checking problems, among which the selection problem recently formulated and proved by Carayol and Serre.

This finitary semantics are inspired from the extensional collapse theorem of Ehrhard, who shows that the relational semantics of linear logic collapses extensionally to the finitary semantics provided by Scott lattices. For that reason, we start in a preliminary approach to define the coloring comonad and the inductive-coinductive fixpoint operator in the quantitative semantics provided by an infinitary (and non-continuous) version of the relational model of linear logic.



Dans cette thèse, nous envisageons des problèmes de model-checking d'ordre supérieur à l'aide d'approches issues de la sémantique et de la logique. Le model-checking d'ordre supérieur étudie la vérification de propriétés, exprimées en logique monadique du second ordre, sur des arbres infinis générés par une classe de systèmes de réécriture appelés schémas de récursion d'ordre supérieur. Ces systèmes sont équivalents au λ-calcul simplement typé avec récursion, et peuvent donc être étudiés à l'aide d'outils sémantiques.

Plus précisément, l'objet de cette thèse est de relier le model-checking d'ordre supérieur à une série de concepts de premier plan en sémantique contemporaine, tels que la logique linéaire et sa sémantique relationnelle, la logique linéaire indexée, les lois distributives entre comonades, les comonades paramétrées et la logique tensorielle. Nous verrons que ces concepts contribuent de façon particulièrement naturelle à l'étude du model-checking d'ordre supérieur.

Notre approche débute par une étude du système de types intersection de Kobayashi et Ong, qui permet de typer un schéma de récursion d'ordre supérieur avec les états d'un automate donné encodant une formule de la logique monadique du second ordre. Le schéma admet pour type l'état initial de l'automate si et seulement si l'arbre infini qu'il représente satisfait la propriété encodée par l'automate. En dépit de cette adéquation, le système de types de Kobayashi et Ong a été pensé indépendamment de la connexion existant entre les types intersections et les modèles de la logique linéaire, relation observée par Bucciarelli, Ehrhard, de Carvalho et Terui. Nous avons donc cherché à relier ces deux domaines.

Notre analyse nous a permis de définir un système de types intersection dérivé de celui de Kobayashi et Ong, capturant lui aussi le model-checking d'ordre supérieur de façon adéquate. Contrairement au système original, notre système est formulé de façon modale, et correspond à une sémantique finitaire de la logique linéaire obtenue en composant la modalité exponentielle usuelle avec une comonade colorant les formules. Nous équipons cette sémantique de la logique linéaire avec un opérateur de point fixe inductif-coinductif, et obtenons ainsi un modèle du λ-calcul avec récursion dans lequel l'interprétation d'un schéma de récursion d'ordre supérieur est l'ensemble des états depuis lesquels l'arbre infini qu'il représente est accepté. La finitude de la sémantique nous permet de donner de nouvelles preuves de plusieurs résultats de décidabilité pour des problèmes de model-checking d'ordre supérieur, dont le problème de la sélectionœ formulé récemment par Carayol et Serre.

La sémantique finitaire que nous définissons est inspirée du théorème d'écrasement extensionnel d'Ehrhard, qui montre que l'écrasement extensionnel du modèle relationnel de la logique linéaire correspond à sa sémantique finitaire donnée par le modèle de Scott. Ce résultat nous permet de définir dans un premier temps la comonade de coloration et l'opérateur de point fixe inductif-coinductif dans une sémantique quantitative correspondant à une variante infinie (et non-continue) du modèle relationnel de la logique linéaire.