Sujet de la thèse : Sémantique de langages de programmation fonctionnels réactifs avec effets

Début de la thèse : 01/10/2021

Directeur de thèse : Frédéric LOULERGUE

Co-encadrant de thèse : Jules CHOUQUET

Résumé :

La programmation réactive fonctionnelle (FRP) est un paradigme fonctionnel élaboré dans le but de simplifier la programmation de systèmes qui interagissent continuellement avec leur environnement. Yampa est une bibliothèque particulièrement importante de ce paradigme. Elle permet aux utilisateurs de construire des fonctions de signal qui traitent de manière synchrone les flux d'entrée pour produire des flux de sortie. Malgré une construction concise et élégante de programme dans Yampa, la gestion des entrées/sorties est un point difficile qui a amené au questionnement sur les effets de bords dans un langage FRP à la Yampa.
Parmi les solutions proposées par la communauté scientifique, nous nous sommes focalisés sur le langage Wormholes défini par Winograd-Cort et Hudak en 2012. Ce langage ajoute des constructions supplémentaires à Yampa permettant d'introduire naturellement des effets dans un programme. Nous avons remarqué des problèmes dans la formalisation ainsi que des limitations non-nécessaires sur l'utilisation des effets.
Dans cette thèse, nous proposons une mécanisation en Rocq d'une variante du langage Wormholes corrigeant les problèmes de la formalisation papier initiale et nous étendons ses concepts dans un nouveau langage nommé Molholes