Fiche de NIGRON Pierre

Titre : Effectful programs and their proofs in type theory : application to certified compilation and certified packet processing
Date : 17 novembre 2022
Heure: 10:00
Résumé : Dans cette thèse, nous nous intéressons d’abord à l’utilisation de la logique de sépa- ration pour raisonner sur des programmes définis dans un variant de la monade libre et 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édicat défini dans une lo- gique de séparation puis à développer une logique de Hoare. Nous nous concentrons sur la fraîcheur et sur l’aspect zéro-copie des bibliothèques d’analyseurs syntaxique. Pour étu- dier 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, dans l’objectif de compiler les analyseurs produits vers C, nous proposons une méthode par raffinement dont l’un des objectifs est de supprimer les continuations introduites par l’utilisation d’une monade libre.
Lieu : Université de Paris