Sémantique de langages de programmation fonctionnels réactifs avec effets

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.