Description
Date depot: 31 mars 2025
Titre: Machines Co-inductives Monadiques pour la Programmation Probabiliste Certifiée
Directrice de thèse:
Christine TASSON (LIP6)
Encadrant :
Frédéric PESCHANSKI (LIP6)
Encadrant :
Romain DEMANGEON (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Programmation et architecture logicielle
Resumé: Ce projet s’inscrit dans le domaine de la programmation certifiée : le développement de programmes dont les propriétés fondamentales de fonctionnement sont garanties par construction. Nous nous plaçons pour cela dans le cadre de la théorie des types dépendants et des assistants de preuve. Le ou la future doctorante pourra s'appuyer sur une formalisation récente de l'approche Event B de la preuve de programmes réactifs en Lean 4. Nous proposons pour cela d'utiliser une approche monadique pour aborder la formalisation coinductive des calculs de flot. Nous pourrons alors démontrer l'efficacité de cette formalisation dans le cadre de la programmation réactive probabiliste qui mélange les aspects réactifs, concurrents et probabilistes.