[1] 
Timothy Bourke, Lélio Brun, PierreÉvariste Dagand, Xavier Leroy, Marc
Pouzet, and Lionel Rieg.
A Formally Verified Compiler for Lustre.
In International Conference on Programming Language, Design and
Implementation (PLDI), Barcelona, Spain, June 1921 2017. ACM.
[ bib 
.pdf ]
The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs. We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where pro grams manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimiza tion that eliminates unnecessary conditional statements.

[2] 
Albert Benveniste, Benoit Caillaud, Hilding Elmqvist, Khalil Ghorbal, Martin
Otter, and Marc Pouzet.
Structural Analysis of MultiMode DAE Systems.
In International Conference on Hybrid Systems: Computation and
Control (HSCC), Pittsburgh, USA, April 1820 2017. ACM.
[ bib 
.pdf ]
Differential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica, VHDLAMS, or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multimode DAE (mDAE) systems are much harder to deal with, not only because of their modedependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs does not cover the multimode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.

[3] 
Timothy Bourke, PierreÉvariste Dagand, Marc Pouzet, and Lionel Rieg.
Vérification de la génération modulaire du code impératif
pour lustre.
In Journées Francophones des Langages Applicatifs (JLFA),
Gourette, Pyrénées, France, January 2017.
[ bib 
.pdf ]
Les langages synchrones sont utilisés pour programmer des logiciels de contrôlecommande d'applications critiques. Le langage Scade, utilisé dans l'industrie pour ces applications, est fondé sur le langage Lustre introduit par Caspi et Halbwachs. On s'intéresse ici à la formalisation et la preuve, dans l'assistant de preuve Coq, d'une étape clef de la compilation : la traduction de programmes Lustre vers des programmes d'un langage impératif. Le défi est de passer d'une sémantique synchrone flot de données, où un programme manipule des flots, à une sémantique impérative, où un programme manipule la mémoire de façon séquentielle. Nous spécifions et vérifions un générateur de code simple qui gère les traits principaux de Lustre : l'échantillonnage, les noeuds et les délais. La preuve utilise un modèle sémantique intermédiaire qui mélange des traits flot de données et impératifs et permet de définir un invariant inductif essentiel. Nous exploitons la formalisation proposée pour vérifier une optimisation classique qui fusionne des structures conditionnelles dans le code impératif généré.

[4] 
Albert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, and Marc
Pouzet.
A Typebased Analysis of Causality Loops in Hybrid Systems
Modelers.
Journal of Nonlinear Analysis Hybrid Systems, 2017.
In press. Selected paper from HSCC'14.
[ bib ]
Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete and continuoustime behaviors with complex interactions between them. An important step in their compilation is the static detection of algebraic or causality loops. Such loops can cause simulations to deadlock and prevent the generation of statically scheduled code. This paper addresses this issue for a hybrid modeling language that combines synchronous dataflow equations with Ordinary Differential Equations (ODEs). We introduce the operator last(x) for the leftlimit of a signal x. The last(x) operator is used to break causality loops and permits a uniform treatment of discrete and continuous state variables. The semantics of the language relies on nonstandard analysis, defining an execution as a sequence of infinitesimally small steps. A signal is deemed causally correct when it can be computed sequentially and only changes infinitesimally outside of announced discrete events like zerocrossings. The causality analysis takes the form of a type system that expresses dependencies between signals. In welltyped programs, (i) signals are provably continuous during integration provided that imported external functions are also continuous, and (ii) sequential code can be generated. The effectiveness of the system is illustrated with several examples written in , a like synchronous language extended with ODEs.

[5] 
Guillaume Baudart, Timothy Bourke, and Marc Pouzet.
Soundness of the QuasiSynchronous Abstraction.
In International Conference on Formal Methods in ComputerAided
Design (FMCAD), Mountain View, California, USA, October, 36 2016.
[ bib 
.pdf ]
Many critical realtime embedded systems are implemented as a set of processes that execute periodically with bounded jitter and communicate with bounded transmission delay. The quasisynchronous ab straction was introduced by P. Caspi for modelchecking the safety properties of applications running on such systems. The simplicity of the abstraction is appealing: the only events are process activations; logical steps account for transmission delays; and no process may be activated more than twice between two successive activations of any other. We formalize the relation between the realtime model and the quasisynchronous abstraction by in troducing the notion of a unitary discretization. Even though the abstraction has been applied several times in the literature, we show, surprisingly, that it is not sound for general systems of more than two processes. Our central result is to propose necessary and sufficient conditions on both communication topologies and tim ing parameters to recover soundness.

[6] 
Albert Cohen, Valentin Perrelle, Dumitru PotopButucaru, Marc Pouzet, Elie
Soubiran, and Zhen Zhang.
Hard Real Time and Mixed Time Criticality on OffTheShelf Embedded
MultiCores.
In ERTS, Toulouse, January 2016.
[ bib 
.pdf ]
The paper describes a pragmatic solution to the parallel execution of hard realtime tasks on offtheshelf embedded multiprocessors. We propose a simple timing isolation protocol allowing computational tasks to communicate with hard realtime ones. Excellent parallel resource utilization can be achieved while preserving timing compositionality. An extension to a synchronous language enables the correctbyconstruction compilation to efficient parallel code. We do not explicitly address certification issues at this stage, yet our approach is designed to enable full system certification at the highest safety standards, such as SIL 4 in IEC 61508 or DAL A in DO178B.

[7]  Marc Pouzet. Building a Hybrid Systems Modeler on Synchronous Languages Principles. In ACM International Conference on Embedded Software (EMSOFT), Amsterdam, October 49 2015. Invited talk. [ bib  .pdf ] 
[8] 
Louis Mandel, Cédric Pasteur, and Marc Pouzet.
ReactiveML, Ten Years Later.
In ACM International Conference on Principles and Practice of
Declarative Programming (PPDP), Siena, Italy, July 2015.
Invited paper for PPDP'05 award.
[ bib 
.pdf ]
Ten years ago we introduced ReactiveML, an extension of a strict ML language with synchronous parallelism a` la Esterel to program reactive applications. Our purpose was to demonstrate that synchronous language principles, originally invented and used for critical realtime control software, would integrate well with ML and prove useful in a wider context: reactive applications with complex data structures and sequential algorithms, organized as a dynamically evolving set of tightly synchronized parallel tasks.

[9] 
Timothy Bourke, JeanLouis Colaço, Bruno Pagano, Cédric Pasteur, and Marc
Pouzet.
A Synchronousbased Code Generator For Explicit Hybrid Systems
Languages.
In International Conference on Compiler Construction (CC),
LNCS, London, UK, April 1118 2015.
[ bib 
.pdf ]
Modeling languages for hybrid systems are cornerstones of embedded systems development in which software interacts with a physical environment. Sequential code generation from such languages is important for simulation efficiency and for producing code for embedded targets. Despite being routinely used in industrial compilers, code generation is rarely, if ever, described in full detail, much less formalized. Yet formalization is an essential step in building trustable compilers for critical embedded software development.

[10] 
Louis Mandel, Cédric Pasteur, and Marc Pouzet.
Time Refinement in a Functional Synchronous Language.
Science of Computer Programming, 2015.
Available online 10 July 2015.
[ bib 
.pdf ]
Concurrent and reactive systems often exhibit multiple time scales. This situation occurs, for instance, in the discrete simulation of a sensor network where the time scale at which agents communicate is very different from the time scale used to model the internals of an agent.

[11] 
Albert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, and Marc
Pouzet.
A Typebased Analysis of Causality Loops in Hybrid Systems
Modelers.
In International Conference on Hybrid Systems: Computation and
Control (HSCC), Berlin, Germany, April 1517 2014. ACM.
[ bib 
.pdf ]
Explicit hybrid systems modelers like Simulink/Stateflow allow for programming both discrete and continuoustime behaviors with complex interactions between them. A key issue in their compilation is the static detection of algebraic or causality loops. Such loops can cause simulations to deadlock and prevent the generation of statically scheduled code.

[12] 
Guillaume Baudart, Florent Jacquemard, Louis Mandel, and Marc Pouzet.
A Synchronous Embedding of Antescofo, a DomainSpecific Language for
Interactive Mixed Music.
In ACM, editor, International Conference on Embedded Software
(EMSOFT), Montreal, September 29October 04 2013.
[ bib 
.pdf ]
Antescofo is a recently developed software for musical score following and mixed music: it automatically, and in realtime, synchronizes electronic instruments with a musician playing on a classical instrument. Therefore, it faces some of the same major challenges as embedded systems. The system provides a programming language used by the composers to specify musical pieces that mix interacting electronic and classical instruments. This language is developed with and for musicians, it continues to evolve according to their needs. Yet, its formal semantics has only recently been formally defined. This paper presents a synchronous semantics for the core language of Antescofo and an alternative implementation, based on an embedding inside an existing synchronous language, namely ReactiveML. The semantics reduces to a few rules, is mathematically precise and leads to an interpretor of a few hundred lines whose efficiency compares well with that of the current implementation. On all musical pieces we have tested, response times have been less than the reaction time of the human ear. Moreover, this embedding permitted the prototyping of several new programming constructs, some of which are described in this paper.

[13] 
Guillaume Baudart, Louis Mandel, and Marc Pouzet.
Programming Mixed Music in ReactiveML.
In Workshop on Functional Art, Music, Modeling and Design
(FARM), Boston, September 28 2013.
Colocated with ICFP 2013.
[ bib 
.pdf ]
Mixed music is about live musicians interacting with electronic parts which are controlled by a computer during the performance. It allows composers to use and combine traditional instruments with complex synthesis sounds and other electronic devices. There are several languages dedicated to the writing of mixed music scores. Among them, the Antescofo language coupled with an advanced score follower allows a composer to manage the reactive aspects of musical performances: how electronic parts interact with a musician. However these domain specific languages do not offer the expressiveness of functional programming. We embed the Antescofo language in a reactive functional pro gramming language, ReactiveML. This approach offers to the com poser recursivity, higher order, inductive types, among others as well as a simple way to program complex reactive behaviors thanks to the synchronous parallel model on which ReactiveML is built. This article presents how to program mixed music in ReactiveML through several examples.

[14] 
Louis Mandel, Cédric Pasteur, and Marc Pouzet.
Time Refinement in a Functional Synchronous Language.
In 15th International Symposium on Principles and Practice of
Declarative Programming (PPDP), Madrid, Spain, September 1618 2013.
[ bib 
.pdf ]
Concurrent and reactive systems often exhibit multiple time scales. For instance, in a discrete simulation, the scale at which agents communicate might be very different from the scale used to model the internals of each agent. We propose an extension of the synchronous model of concurrency, called reactive domains, to simplify the pro gramming of such systems. Reactive domains allow the creation of local time scales and enable refinement, that is, the replacement of an approximation of a system with a more detailed version without changing its behavior as observed by the rest of the program. Our work is applied to the ReactiveML language, which extends ML with synchronous language constructs. We pre sent an operational semantics for the extended language and a type system that ensures the soundness of programs.

[15]  Timothy Bourke and Marc Pouzet. Zélus, a Hybrid Synchronous Language. École normale supérieure, September 2013. Distribution at: zelus.di.ens.fr. [ bib  http ] 
[16]  Timothy Bourke and Marc Pouzet. SundialsML: an ML binding for Sundials CVODE. École normale supérieure, September 2013. Distribution at: zelus.di.ens.fr. [ bib  http ] 
[17] 
Timothy Bourke and Marc Pouzet.
Zélus, a Synchronous Language with ODEs.
In International Conference on Hybrid Systems: Computation and
Control (HSCC 2013), Philadelphia, USA, April 811 2013. ACM.
[ bib 
.pdf ]
Zélus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user's perspective, its main originality is to extend an existing Lustrelike synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as dataflow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code.

[18] 
Albert Cohen, Léonard Gérard, and Marc Pouzet.
Programming parallelism with futures in Lustre.
In ACM International Conference on Embedded Software
(EMSOFT'12), Tampere, Finland, October 712 2012. ACM.
Best paper award.
[ bib 
.pdf ]
Efficiently distributing synchronous programs is a challenging and longstanding subject. This paper introduces the use of futures in a Lustrelike language, giving the programmer control over the expression of parallelism. In the synchronous model where computations are considered instantaneous, futures increase expressiveness by decoupling the beginning from the end of a computation.

[19] 
Léonard Gérard, Adrien Guatto, Cédric Pasteur, and Marc Pouzet.
A Modular Memory Optimization for Synchronous DataFlow Languages.
Application to Arrays in a Lustre Compiler.
In Languages, Compilers and Tools for Embedded Systems
(LCTES'12), Beijing, June 1213 2012. ACM.
Best paper award.
[ bib 
.pdf ]
The generation of efficient sequential code for synchronous dataflow languages raises two intertwined issues: control and memory optimization. While the former has been extensively studied, for instance in the compilation of Lustre and SIGNAL, the latter has been only addressed in a restricted manner. Yet, memory optimization becomes a pressing issue when arrays are added to such languages.

[20] 
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet.
NonStandard Semantics of Hybrid Systems Modelers.
Journal of Computer and System Sciences (JCSS), 78(3):877910,
May 2012.
Special issue in honor of Amir Pnueli.
[ bib 
DOI 
.pdf ]
Hybrid system modelers have become a corner stone of complex embedded system development. Embedded systems include not only control components and software, but also physical devices. In this area, Simulink is a de facto standard design framework, and Modelica a new player. However, such tools raise several issues related to the lack of reproducibility of simulations (sensitivity to simulation parameters and to the choice of a simulation engine).

[21] 
Louis Mandel, Florence Plateau, and Marc Pouzet.
Static Scheduling of Latency Insensitive Designs with Lucyn.
In International Conference on Formal Methods in ComputerAided
Design (FMCAD), Austin, Texas, USA, October 30  November 2 2011.
[ bib 
.pdf ]
Lucyn is a dataflow programming language similar to Lustre extended with a buffer operator. It is based on the nsynchronous model which was initially introduced for programming multimedia streaming applications. In this article, we show that Lucyn is also applicable to model Latency Insensitive Designs (LID). In order to model latency introduced by wires, we add a delay operator. Thanks to this new operator, a LID can be described by a Lucyn program. Then, the Lucyn compiler automatically provides static schedules for computation nodes and buffer sizes needed in shell wrappers.

[22] 
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet.
A Hybrid Synchronous Language with Hierarchical Automata: Static
Typing and Translation to Synchronous Code.
In ACM SIGPLAN/SIGBED Conference on Embedded Software
(EMSOFT'11), Taipei, Taiwan, October 2011.
[ bib 
.pdf ]
Hybrid modeling tools such as Simulink have evolved from simulation platforms into development platforms on which simulation, testing, formal verification and code generation are performed. It is thus critical to place them on a firm semantical basis where it can be proven that the results of simulation, compilation and verification are mutually consistent. Synchronous languages have addressed these issues but only for discrete systems. They cannot be used to model hybrid systems with both efficiency and precision.

[23] 
Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet.
Divide and recycle: types and compilation for a hybrid synchronous
language.
In ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools
and Theory for Embedded Systems (LCTES'11), Chicago, USA, April 2011.
[ bib 
.pdf ]
Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

[24] 
Albert Benveniste, Benoit Caillaud, and Marc Pouzet.
The Fundamentals of Hybrid Systems Modelers.
In 49th IEEE International Conference on Decision and Control
(CDC), Atlanta, Georgia, USA, December 1517 2010.
[ bib 
.pdf ]
Hybrid systems modelers have become the corner stone of embedded system development, with Simulink a de facto standard and Modelica a new player. Such tools still raise a number of issues that, we believe, require more fundamental understanding.

[25] 
Louis Mandel, Florence Plateau, and Marc Pouzet.
Lucyn: a nSynchronous Extension of Lustre.
In 10th International Conference on Mathematics of Program
Construction (MPC'10), Manoir StCastin, Québec, Canada, June 2010.
Springer LNCS.
[ bib 
.pdf ]
Synchronous functional languages such as Lustre or Lucid Synchrone define a restricted class of Kahn Process Networks which can be executed with no buffer. Every expression is associated to a clock indicating the instants when a value is present. A dedicated type system, the clock calculus, checks that the actual clock of a stream equals its expected clock and thus does not need to be buffered. The nsynchrony relaxes synchrony by allowing the communication through bounded buffers whose size is computed at compiletime. It is obtained by extending the clock calculus with a subtyping rule which defines buffering points.

[26]  Louis Mandel, Florence Plateau, and Marc Pouzet. Lucyn: a nSynchronous Extension of Lustre. Workshop on Designing Correct Circuits (DCC 10)  ETAPS, March 2010. [ bib ] 
[27] 
Marc Pouzet and Pascal Raymond.
Modular Static Scheduling of Synchronous Dataflow Networks: An
efficient symbolic representation.
Journal of Design Automation for Embedded Systems,
3(14):165192, 2010.
Special issue of selected papers from
Embedded System Week. Extended version
of [29].
[ bib 
http 
.pdf ]
This paper addresses the question of producing modular sequential imperative code from synchronous dataflow networks. Precisely, given a system with several input and output flows, how to decompose it into a minimal number of classes executed atomically and statically scheduled without restricting possible feedback loops between input and output? Though this question has been identified by Raymond in the early years of LUSTRE, it has almost been left aside until the recent work of Lublinerman, Szegedy and Tripakis. The problem is proven to be intractable, in the sense that it belongs to the family of optimization problems where the corresponding decision problem  there exists a solution with size c  is NPcomplete. Then, the authors derive an iterative algorithm looking for solutions for c = 1, 2,... where each step is encoded as a satisfiability (SAT) problem.

[28]  Louis Mandel, Florence Plateau, and Marc Pouzet. Lucyn: une extension nSynchrone de Lustre. In Journées Francophones des Langages Applicatifs (JFLA), La Ciota, France, Janvier 2010. INRIA. [ bib ] 
[29] 
Marc Pouzet and Pascal Raymond.
Modular Static Scheduling of Synchronous Dataflow Networks: An
efficient symbolic representation.
In ACM International Conference on Embedded Software
(EMSOFT'09), Grenoble, France, October 2009.
[ bib 
.pdf ]
This paper addresses the question of producing modular sequential imperative code from synchronous dataflow networks. Precisely, given a system with several input and output flows, how to decompose it into a minimal number of classes executed atomically and statically scheduled without restricting possible feedback loops between input and output? Though this question has been identified by Raymond in the early years of Lustre, it has almost been left aside until the recent work of Lublinerman, Szegedy and Tripakis. The problem is proven to be intractable, in the sense that it belongs to the family of optimization problems where the corresponding decision problem  there exists a solution with size c  is NPcomplete. Then, the authors derive an iterative algorithm looking for solutions for c = 1,2,... where each step is encoded as a SAT problem.

[30] 
Paul Caspi, JeanLouis Colaço, Léonard Gérard, Marc Pouzet, and Pascal
Raymond.
Synchronous Objects with Scheduling Policies: Introducing safe
shared memory in Lustre.
In ACM International Conference on Languages, Compilers, and
Tools for Embedded Systems (LCTES), Dublin, June 2009.
[ bib 
.pdf ]
This paper addresses the problem of designing and implementing complex control systems for realtime embedded software. Typical applications involve different control laws corresponding to different phases or modes, e.g., takeoff, full flight and landing in a flybywire control system. On one hand, existing methods such as the combination of Simulink/Stateflow provide powerful but unsafe mechanisms by means of imperative updates of shared variables. On the other hand, synchronous languages and tools such as Esterel or Scade/Lustre are too restrictive and forbid to fully separate the specification of modes from their actual instantiation with a particular control automaton.

[31]  Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet. Relaxing Synchronous Composition with Clock Abstraction. Workshop on Hardware Design using Functional languages (HFL 09)  ETAPS, 2009. [ bib  http ] 
[32] 
Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet.
Abstraction of Clocks in Synchronous Dataflow Systems.
In The Sixth ASIAN Symposium on Programming Languages and
Systems (APLAS), Bangalore, India, December 2008.
[ bib 
.pdf ]
Synchronous dataflow languages such as Lustre manage infinite sequences or streams as basic values. Each stream is associated to a clock which defines the instants where the current value of the stream is present. This clock is a type information and a dedicated type system  the socalled clockcalculus  statically rejects programs which cannot be executed synchronously. In existing synchronous languages, it amounts at asking whether two streams have the same clocks and thus relies on clock equality only. Recent works have shown the interest of introducing some relaxed notion of synchrony, where two streams can be composed as soon as they can be synchronized through the introduction of a finite buffer (as done in the SDF model of Edward Lee). This technically consists in replacing typing by subtyping. The present paper introduces a simple way to achieve this relaxed model through the use of clock envelopes. These clock envelopes are set of concrete clocks which are not necessarily periodic. This allows to model various features in realtime embedded software such as bounded jitter as found in videosystems, execution time of realtime processes and scheduling resources or the communication through buffers. We present the algebra of clock envelopes and its main theoretical properties.

[33] 
Gwenael Delaval, Alain Girault, and Marc Pouzet.
A Type System for the Automatic Distribution of Higherorder
Synchronous Dataflow Programs.
In ACM International Conference on Languages, Compilers, and
Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008.
[ bib 
.pdf ]
We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architecture and functional modularity, our first contribution is to extend an existing synchronous dataflow programming language with primitives allowing the description of a distributed architecture and the localization of some expressions onto some processors. We also present a distributed semantics to formalize the distributed execution of synchronous programs. Our second contribution is to provide a type system, in order to infer the localization of nonannotated values by means of type inference and to ensure, at compilation time, the consistency of the distribution. Our third contribution is to provide a typedirected projection operation to obtain automatically, from a centralized typed program, the local program to be executed by each computing resource. The type system as well as the automatic distribution mechanism has been fully implemented in the compiler of an existing synchronous dataflow programming language.

[34] 
Darek Biernacki, JeanLouis Colaco, Grégoire Hamon, and Marc Pouzet.
Clockdirected Modular Code Generation of Synchronous Dataflow
Languages.
In ACM International Conference on Languages, Compilers, and
Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008.
[ bib 
.pdf ]
The compilation of synchronous block diagrams into sequential imperative code has been addressed in the early eighties and can now be considered as folklore. However, modular code generation, though largely used in existing compilers and particularly in industrial ones, has never been precisely described or entirely formalized. Such a formalization is now fundamental in the longterm goal to develop a mathematically certified compiler for a synchronous language as well as in simplifying existing implementations.

[35]  Louis Mandel and Florence Plateau. Interactive programming of reactive systems. In Proceedings of Modeldriven Highlevel Programming of Embedded Systems (SLA++P'08), Budapest, Hungary, April 2008. [ bib  .pdf ] 
[36]  Paul Caspi, JeanLouis Colaço, and Marc Pouzet. Objects in BlockDiagram Languages, January 2008. Unpublished. [ bib ] 
[37]  Louis Mandel and Marc Pouzet. ReactiveML : un langage fonctionnel pour la programmation réactive. Techniques et Sciences Informatiques (TSI), 2008. [ bib  .pdf ] 
[38]  Sébastien Labbé, JeanPierre Gallois, and Marc Pouzet. Slicing communicating automata specifications for efficient model reduction. In 18th Australian Conference on Software Engineering (ASWEC), 2007. [ bib ] 
[39] 
Paul Caspi, Grégoire Hamon, and Marc Pouzet.
RealTime Systems: Models and verification  Theory and
tools, chapter Synchronous Functional Programming with Lucid Synchrone.
ISTE, 2007.
English translation of [46].
[ bib 
.pdf ]
Lucid Synchrone is a programming language dedicated to the design of reactive systems. It is based on the synchronous model of Lustre which it extends with features usually found in functional languages such as higherorder or constructed datatypes. The language is equipped with several static analysis, all expressed as special typesystems and used to ensure the absence of certain runtime errors on the final application. It provides, in particular, automatic type and clock inference and statically detects initialization issues or deadlocks. Finally, the language offers both dataflow and automatabased programming inside a unique framework.

[40]  Darek Biernacki, JeanLouis Colaco, and Marc Pouzet. Clockdirected Modular Compilation from Synchronous Blockdiagrams. In Workshop on Automatic Program Generation for Embedded Systems (APGES), Salzburg, Austria, october 2007. Embedded System Week. [ bib  .pdf ] 
[41] 
Farid Benbadis, Louis Mandel, Marc Pouzet, and Ludovic Samper.
Simulation of Ad hoc Networks in ReactiveML.
Submitted to journal publication, Feb 2007.
[ bib 
.pdf ]
This paper presents a programming experiment of complex network routing protocols for mobile ad hoc networks within the reactive language ReactiveML.

[42] 
JeanLouis Colaço, Grégoire Hamon, and Marc Pouzet.
Mixing Signals and Modes in Synchronous Dataflow Systems.
In ACM International Conference on Embedded Software
(EMSOFT'06), Seoul, South Korea, October 2006.
[ bib 
.pdf ]
Synchronous dataflow languages such as SCADE/Lustre manage infinite sequences or streams as primitive values making them naturally adapted to the description of datadominated systems. Their conservative extension with means to define controlstructures or modes have been a longterm research topic and several solutions have emerged.

[43]  Marc Pouzet. Lucid Synchrone, version 3. Tutorial and reference manual. Université ParisSud, LRI, April 2006. [ bib ] 
[44]  Alain Girault, Xavier Nicollin, and Marc Pouzet. Automatic Rate Desynchronization of Embedded Reactive Programs. ACM Transactions on Embedded Computing Systems (TECS), 5(3), 2006. [ bib ] 
[45] 
Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence
Plateau, and Marc Pouzet.
NSynchronous Kahn Networks: a Relaxed Model of Synchrony for
RealTime Systems.
In ACM International Conference on Principles of Programming
Languages (POPL'06), Charleston, South Carolina, USA, January 2006.
[ bib 
.pdf ]
The design of highperformance streamprocessing systems is a fast growing domain, driven by markets such like highend TV, gaming, 3D animation and medical imaging. It is also a surprisingly demanding task, with respect to the algorithmic and conceptual simplicity of streaming applications. It needs the close cooperation between numerical analysts, parallel programming experts, realtime control experts and computer architects, and incurs a very high level of quality insurance and optimization.

[46] 
Paul Caspi, Grégoire Hamon, and Marc Pouzet.
Systèmes Tempsréel : Techniques de Description et de
Vérification  Théorie et Outils, volume 1, chapter Lucid Synchrone,
un langage de programmation des systèmes réactifs, pages 217260.
Hermes, 2006.
[ bib 
.pdf ]
Ce chapitre présente Lucid Synchrone, un langage dédié à la programmation de systèmes réactifs. Il est fondé sur le modèle synchrone de Lustre qu'il étend avec des caractéristiques présentes dans les langages fonctionnels tels que l'ordre supérieur ou l'inférence des types. Il offre un mécanisme de synthèse automatique des horloges et permet de décrire, dans un cadre unifié, une programmation flot de données et une programmation par automates.

[47]  Louis Mandel. Conception, Sémantique et Implantation de ReactiveML : un langage à la ML pour la programmation réactive. PhD thesis, Université Paris 6, 2006. [ bib ] 
[48]  Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchroning Periodic Clocks. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib  .pdf ] 
[49] 
JeanLouis Colaço, Bruno Pagano, and Marc Pouzet.
A Conservative Extension of Synchronous Dataflow with State
Machines.
In ACM International Conference on Embedded Software
(EMSOFT'05), Jersey city, New Jersey, USA, September 2005.
[ bib 
.pdf ]
This paper presents an extension of a synchronous dataflow language such as Lustre with imperative features expressed in terms of powerful state machine à la SyncChart. This extension is fully conservative in the sense that all the programs from the basic language still make sense in the extended language and their semantics is preserved.

[50] 
Louis Mandel and Marc Pouzet.
ReactiveML, a Reactive Extension to ML.
In ACM International Conference on Principles and Practice of
Declarative Programming (PPDP), Lisboa, July 2005.
Recipient of the price for the “most influential PPDP'05 paper”
given in July 2015 at PPDP'15.
[ bib 
.pdf ]
We present ReactiveML, a programming language dedicated to the implementation of complex reactive systems as found in graphical user interfaces, video games or simulation problems. The language is based on the reactive model introduced by Boussinot. This model combines the socalled synchronous model found in Esterel which provides instantaneous communication and parallel composition with classical features found in asynchronous models like dynamic creation of processes.

[51] 
Louis Mandel et Marc Pouzet.
ReactiveML, un langage pour la programmation réactive en ML.
In Journées Francophones des Langages Applicatifs (JFLA),
Obernai, France, Mars 2005. INRIA.
[ bib 
.ps.gz ]
Nous présentons ReactiveML, un langage dédié à la programmation de systèmes réactifs complexes tels que les interfaces graphiques, les jeux vidéo ou les problèmes de simulation. Le langage est basé sur le modèle réactif synchrone introduit dans les années 90 par Frédéric Boussinot. Ce modèle combine les principes du modèle synchrone avec la possibilité de créer dynamiquement des processus.

[52] 
Louis Mandel and Farid Benbadis.
Simulation of Mobile AdHoc Networks in ReactiveML.
In Electronic Notes in Theoretical Computer Science, editor,
Synchronous Languages, Applications, and Programming (SLAP), 2005.
available at wwwspi.lip6.fr/~mandel/rml.
[ bib 
.ps.gz ]
This paper presents a programming experiment of a complex network routing protocol for mobile ad hoc networks within the ReactiveML language.

[53]  JeanLouis Colaço and Marc Pouzet. Typebased Initialization Analysis of a Synchronous Dataflow Language. International Journal on Software Tools for Technology Transfer (STTT), 6(3):245255, August 2004. [ bib  .pdf ] 
[54]  Grégoire Hamon. Synchronous Dataflow Pattern Matching. In Synchronous Languages, Applications, and Programming. Electronic Notes in Theoretical Computer Science, 2004. [ bib  .ps.gz ] 
[55] 
JeanLouis Colaço, Alain Girault, Grégoire Hamon, and Marc Pouzet.
Towards a Higherorder Synchronous Dataflow Language.
In ACM Fourth International Conference on Embedded Software
(EMSOFT'04), Pisa, Italy, september 2004.
[ bib 
.pdf ]
The paper introduces a higherorder synchronous dataflow language in which communication channels may themselves transport programs. This provides a mean to dynamically reconfigure dataflow processes. The language comes as a natural and strict extension of both Lustre and Lucid Synchrone. This extension is conservative, in the sense that a firstorder restriction of the language can receive the same semantics. We illustrate the expressivity of the language with some examples, before giving the formal semantics of the underlying calculus. The language is equipped with a polymorphic type system allowing types to be automatically inferred and a clock calculus rejecting programs for which synchronous execution cannot be statically guaranteed. To our knowledge, this is the first higherorder synchronous dataflow language where stream functions are first class citizens.

[56] 
JeanLouis Colaço and Marc Pouzet.
Clocks as First Class Abstract Types.
In Third International Conference on Embedded Software
(EMSOFT'03), Philadelphia, Pennsylvania, USA, october 2003.
[ bib 
.ps.gz ]
Clocks in synchronous dataflow languages are the natural way to define several time scales in reactive systems. They play a fundamental role during the specification of the system and are largely used in the compilation process to generate efficient sequential code. Based on the formulation of clocks as dependent types, the paper presents a simpler clock calculus reminiscent to ML type systems with first order abstract types à la Laufer & Odersky. Not only this system provides clock inference, it shares efficient implementations of ML type systems and appears to be expressive enough for many real applications.

[57]  Paul Caspi and Marc Pouzet. Lucid Synchrone, a functional extension of Lustre. Submitted to publication, 2002. [ bib ] 
[58] 
JeanLouis Colaço and Marc Pouzet.
Typebased Initialization Analysis of a Synchronous Dataflow
Language.
In Synchronous Languages, Applications, and Programming,
volume 65. Electronic Notes in Theoretical Computer Science, 2002.
[ bib 
.ps.gz ]
One of the appreciated features of the synchronous dataflow approach is that a program defines a perfectly deterministic behavior. But the use of the delay primitive leads to undefined values at the first cycle; thus a dataflow program is really deterministic only if it can be shown that such undefined values do not affect the behavior of the system.

[59]  Marc Pouzet. Lucid Synchrone: un langage synchrone d'ordre supérieur. Paris, France, 14 novembre 2002. Habilitation à diriger les recherches. [ bib  .ps.gz ] 
[60] 
Sylvain Boulmé and Grégoire Hamon.
Certifying Synchrony for Free.
In International Conference on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR), volume 2250, La Havana, Cuba, December
2001. Lecture Notes in Artificial Intelligence, SpringerVerlag.
Short version of A clocked denotational semantics for
LucidSynchrone in Coq, available as a Technical Report (LIP6), at
www.di.ens.fr/~pouzet/bib/bib.html.
[ bib 
.ps.gz ]
We express reactive programs in Coq using dataflow synchronous operators. Following Lucid Synchrone approach, synchronous static constraints are here expressed using dependent types. Hence, our analysis of synchrony is here directly performed by Coq typechecker.

[61]  Marc Pouzet. Lucid Synchrone, version 2. Tutorial and reference manual. Université Pierre et Marie Curie, LIP6, Mai 2001. Distribution available at: www.lri.fr/~pouzet/lucidsynchrone. [ bib ] 
[62] 
Pascal Cuoq and Marc Pouzet.
Modular Causality in a Synchronous Stream Language.
In European Symposium on Programming (ESOP'01), Genova, Italy,
April 2001.
[ bib 
.ps.gz ]
This article presents a causality analysis for a synchronous stream language with higherorder functions. This analysis takes the shape of a type system with rows. Rows were originally designed to add extensible records to the ML type system (Didier Rémy, Mitchell Wand). We also restate briefly the coiterative semantics for synchronous streams (Paul Caspi, Marc Pouzet), and prove the correctness of our analysis with respect to this semantics.

[63] 
Grégoire Hamon and Marc Pouzet.
Modular Resetting of Synchronous Dataflow Programs.
In ACM International conference on Principles of Declarative
Programming (PPDP'00), Montreal, Canada, September 2000.
[ bib 
.ps.gz ]
This paper presents an extension of a synchronous dataflow language providing full functionality with a modular reset operator. This operator can be considered as a basic primitive for describing dynamic reconfigurations in a purely dataflow framework. The extension proposed here is conservative with respect to the fundamental properties of the initial language: reactivity (i.e, execution in bounded memory and time) and referential transparency are kept. The reset operator is thus compatible with higherorder. This is obtained by extending the clock calculus of the initial language and providing a compilation method. We illustrate the use of this operator by describing an automatic encoding of Modeautomata. All the experiments presented in the paper has been done with Lucid Synchrone, an ML extension of Lustre.

[64]  JeanLouis Colaço et Marc Pouzet. Prototypages. Rapport final du projet GENIE II, Verilog SA, Janvier 2000. [ bib ] 
[65]  Paul Caspi and Marc Pouzet. Lucid Synchrone, a functional extension of Lustre. Technical report, Université Pierre et Marie Curie, Laboratoire LIP6, 2000. [ bib ] 
[66]  Paul Caspi and Marc Pouzet. Lucid Synchrone: une extension fonctionnelle de Lustre. In Journées Francophones des Langages Applicatifs (JFLA), MorzineAvoriaz, Février 1999. INRIA. [ bib  .ps.gz ] 
[67]  Grégoire Hamon and Marc Pouzet. Un Simulateur Synchrone pour Lucid Synchrone. In Journées Francophones des Langages Applicatifs (JFLA), MorzineAvoriaz, Février 1999. INRIA. [ bib  .ps.gz ] 
[68]  Paul Caspi and Marc Pouzet. Lucid Synchrone, version 1.01. Tutorial and reference manual. Laboratoire d'Informatique de Paris 6, January 1999. [ bib ] 
[69]  Paul Caspi and Marc Pouzet. A Coiterative Characterization of Synchronous Stream Functions. In Coalgebraic Methods in Computer Science (CMCS'98), Electronic Notes in Theoretical Computer Science, March 1998. Extended version available as a VERIMAG tech. report no. 9707 at www.di.ens.fr/~pouzet/bib/bib.html. [ bib  .ps.gz ] 
[70]  Paul Caspi and Marc Pouzet. A Coiterative Characterization of Synchronous Stream Functions. Technical Report 07, VERIMAG, October 1997. [ bib  .ps.gz ] 
[71]  Marc Pouzet. Using the parallel complexity of programs to improve compaction. In IEEE International Conference on Parallel Architectures and Compilation Techniques (PACT), Boston, October 1996. [ bib  .ps.gz ] 
[72]  Paul Caspi and Marc Pouzet. Synchronous Kahn Networks. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Philadelphia, Pensylvania, May 1996. [ bib  .ps.gz ] 
[73]  Marc Pouzet. Une présentation fonctionnelle de la compaction de code. Techniques et Sciences Informatiques (TSI), 15(7), 1996. Numéro spécial "langages applicatifs". [ bib  .ps.gz ] 
[74]  Paul Caspi et Marc Pouzet. Réseaux de Kahn Synchrones. In Journées Francophones des Langages Applicatifs (JFLA), Val Morin (Québec), Canada, 2830 janvier 1996. [ bib  .ps.gz ] 
[75]  Marc Pouzet. The Program Compaction Revisited: the Functional Framework. In International Conference on Parallel Processing (EUROPAR'95), LNCS 966, Stockholm, Sweden, August 2931 1995. [ bib  .ps.gz ] 
[76]  Paul Caspi and Marc Pouzet. A Functional Extension to Lustre. In M. A. Orgun and E. A. Ashcroft, editors, International Symposium on Languages for Intentional Programming, Sydney, Australia, May 1995. World Scientific. [ bib  .ps.gz ] 
[77]  Marc Pouzet. Fast compaction of tailrecursive expressions using an abstract distance. Technical Report Spectre953, Verimag, Grenoble, France, February 1995. Available by anonymous ftp on imag.fr in pub/SPECTRE. [ bib ] 
[78]  Marc Pouzet. Fine grain parallelisation of functional programs for VLIW or superscalars architectures. In IFIP WG 10.3 International Conference on Applications in Parallel and Distributed Computing, Caracas,Venezuela, April 1994. [ bib ] 
[79]  Marc Pouzet. Compaction des langages Fonctionnels. PhD thesis, Université Paris VII, sOctober 1994. [ bib ] 
[80]  Marc Pouzet. Parallélisation à grain fin des programmes fonctionnels. In 5ièmes Rencontres du Parallélisme, Brest, France, Mai 1993. [ bib ] 
[81]  Louis Mandel. The ReactiveML distribution. Université ParisSud 11. Available at: rml.lri.fr. [ bib ] 
This file was generated by bibtex2html 1.98.