Direction de recherche : Julia LAWALL

Co-encadrement : DAGAND Pierre-Evariste

Programmes avec effets et leurs preuves dans la théorie des types : application à la compilation certifiée et aux traitements de paquets certifiés

Pour pouvoir raisonner sur nos programmes, une méthode est de directement les écrire dans un assistant de preuve. Utilisant la correspondance de Curry-Howard, les programmes et les preuves ne font alors qu’un. Pour ne pas nuire à la cohérence logique de l’assistant de preuve, le système est obligé de restreindre les programmes à ne pas avoir d’effets de bord. Cependant, les effets de bord sont omniprésents et essentiels dans la programmation. Différentes techniques telles que les monades ou les effets algébriques ont alors émergé pour les modéliser offrant ainsi un moyen d'écrire des programmes impératifs dans des langages purement fonctionnels. C'est donc assez naturellement que les résultats de décennies de recherches investies pour raisonner sur des programmes impératifs tentent d'être adaptés au raisonnement sur des programmes avec effets. Dans cette thèse, nous nous intéressons d'abord à l'utilisation de la logique de séparation pour raisonner sur des programmes avec effets implémentés dans un assistant de preuve. Nous étudions une approche consistant à décrire les comportements des effets à l'aide d'un transformateur de prédicats. Nous nous concentrons d'abord sur la fraîcheur, puis sur le traitement de paquets et le zéro-copie. Pour étudier notre approche, nous nous appuyons sur deux exemples concrets qui sont le module SimplExpr de CompCert et la bibliothèque de décodeur Nom. Pour finir, pour compiler les analyseurs de paquets produits vers C, nous proposons une méthode par raffinement supprimant les continuations introduites par l'utilisation d'une monade libre et effectuant quelques optimisations.

Publications 2021-2022

• 2022
  • P. Nigron : “Programmes avec effets et leurs preuves dans la théorie des types : application à la compilation certifiée et aux traitements de paquets certifiés”, thèse, soutenance 17/11/2022, direction de recherche Lawall, Julia, co-encadrement : Dagand, Pierre-Evariste (2022)
• 2021
  • P. Nigron, P.‑E. Dagand : “Reaching for the Star: Tale of a Monad in Coq”, Leibniz International Proceedings in Informatics, vol. 193, Leibniz International Proceedings in Informatics (LIPIcs), Rome, Italy, pp. 29:1-29:19, (Schloss Dagstuhl) (2021)