Sémantique de langages de programmation fonctionnels réactifs avec effets
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...
Guardat en:
| Autor principal: | |
|---|---|
| Altres autors: | , , , , , , , |
| Format: | Thèse numérique |
| Idioma: | Français |
| Publicat: |
2025.
|
| Matèries: | |
| Accés en línia: | Accès au texte intégral https://theses.univ-orleans.fr/public/2025ORLE1052_va.pdf http://www.theses.fr/2025ORLE1052/abes https://theses.hal.science/tel-05519422 |
| Nota: |
Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes - MIPTIS Partenaire(s) de recherche : LIFO - Laboratoire d'Informatique Fondamentale d'Orléans (Laboratoire) Autre(s) contribution(s) : Sébastien Limet (Président du jury) ; Frédéric Gava, Marc Pouzet, Jules Chouquet, Celia Picard, Timothy Bourke (Membre(s) du jury) ; Frédéric Gava, Marc Pouzet (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Semantics of functional reactive programming languages with effects |
| Sumari: | 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. Functional Reactive Programming (FRP) is a functional programming paradigm designed for systems interacting with their environment. An important branch of this paradigm was introduced by Hudak et al. in 2002 via the Haskell library named YAMPA. It allows users to construct signal functions that synchronously process input streams to produce output streams. While this library facilitates concise and robust coding, managing I/O is cumbersome which led to questions about side effects for YAMPA-like languages. Among the solutions proposed by the scientific community, we focused on the WORMHOLES language defined by Winograd-Cort and Hudak in 2012. This language adds constructs to YAMPA which allows us to simply introduce side effects into a program. We noticed problems in the formalization, as well as unnecessary limitations on the use of effects. In this thesis, we propose a mechanization in ROCQ of a variant of WORMHOLES that corrects the problems found and extends its concepts in a new language named Molholes. |
|---|---|
| Descripció de l’ítem: | Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes - MIPTIS Partenaire(s) de recherche : LIFO - Laboratoire d'Informatique Fondamentale d'Orléans (Laboratoire) Autre(s) contribution(s) : Sébastien Limet (Président du jury) ; Frédéric Gava, Marc Pouzet, Jules Chouquet, Celia Picard, Timothy Bourke (Membre(s) du jury) ; Frédéric Gava, Marc Pouzet (Rapporteur(s)) |
| Format: | Configuration requise : un logiciel capable de lire un fichier au format : PDF |