bib.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib --expand /Users/pouzet/bib/these.bib /Users/pouzet/bib/lucy.bib /Users/pouzet/bib/rml.bib}}
@techreport{pouzet:spectre95,
  author = {Marc Pouzet},
  title = {Fast Compaction of Tail-recursive Expressions using
                 an Abstract Distance},
  institution = {Verimag},
  year = 1995,
  number = {Spectre-95-3},
  month = {February},
  address = {Grenoble, France},
  note = {Available by anonymous ftp on
               {\tt imag.fr} in {\tt pub/SPECTRE}}
}
@phdthesis{pouzet:these94,
  author = {Marc Pouzet},
  title = {Compaction des langages Fonctionnels},
  school = {Universit\'e {Paris VII}},
  year = 1994,
  month = {sOctober}
}
@inproceedings{pouzet:rempar93,
  author = {Marc Pouzet},
  title = {Parall\'elisation \`a Grain Fin des Programmes Fonctionnels},
  booktitle = {5-i\`emes Rencontres du Parall\'elisme},
  year = 1993,
  month = {Mai},
  address = {Brest, France}
}
@inproceedings{pouzet:CAPD94,
  author = {Marc Pouzet},
  title = {Fine Grain Parallelisation of Functional Programs for
                 {VLIW} or Superscalars Architectures},
  booktitle = {IFIP WG 10.3 International Conference on Applications in
                      Parallel and Distributed Computing},
  organisation = {IFIP WG 10.3},
  year = 1994,
  month = {April},
  address = {Caracas,Venezuela}
}
@inproceedings{pouzet:europar95,
  author = {Marc Pouzet},
  title = {{The Program Compaction Revisited: the Functional Framework}},
  booktitle = {International Conference on Parallel Processing
                      (EURO-PAR'95)},
  series = {LNCS 966},
  address = {Stockholm, Sweden},
  year = 1995,
  month = {August 29-31},
  url = {euro-par95.ps.gz}
}
@inproceedings{pouzet:pact96,
  author = {Marc Pouzet},
  title = {Using the Parallel Complexity of Programs to Improve
                 Compaction},
  booktitle = {IEEE International Conference on Parallel
                      Architectures and Compilation Techniques (PACT)},
  year = 1996,
  month = {October},
  address = {Boston},
  url = {pact96.ps.gz}
}
@article{pouzet:tsi96,
  author = {Marc Pouzet},
  title = {Une pr\'esentation fonctionnelle de la compaction de code},
  journal = {Techniques et Sciences Informatiques (TSI)},
  year = 1996,
  volume = 15,
  number = 7,
  note = {Num\'ero sp\'ecial "langages applicatifs"},
  url = {tsi96.ps.gz}
}
@inproceedings{lucy:islip95,
  author = {Paul Caspi and Marc Pouzet},
  title = {{A Functional Extension to Lustre}},
  booktitle = {International Symposium on Languages for
                      Intentional Programming},
  year = 1995,
  month = {May},
  address = {Sydney, Australia},
  editor = {M.~A. Orgun and E.~A. Ashcroft},
  publisher = {World Scientific},
  url = {islip95.ps.gz}
}
@inproceedings{lucy:jfla96,
  author = {Paul Caspi et Marc Pouzet},
  title = {{R\'eseaux de Kahn Synchrones}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 1996,
  month = {28-30 janvier},
  address = {Val Morin (Qu\'ebec), Canada},
  url = {jfla96.ps.gz}
}
@inproceedings{lucy:icfp96,
  author = {Paul Caspi and Marc Pouzet},
  title = {{Synchronous Kahn Networks}},
  booktitle = {ACM SIGPLAN International Conference on
                      Functional Programming (ICFP)},
  year = 1996,
  month = {May},
  address = {Philadelphia, Pensylvania},
  url = {icfp96.ps.gz}
}
@inproceedings{lucy:cmcs98,
  author = {Paul Caspi and Marc Pouzet},
  title = {{A Co-iterative Characterization of 
                  Synchronous Stream Functions}},
  booktitle = {Coalgebraic Methods in Computer Science 
                 (CMCS'98)},
  series = {Electronic Notes in Theoretical Computer Science},
  year = 1998,
  month = {March},
  note = {Extended version available as a VERIMAG tech. report
                  no. 97--07 at {\tt www.di.ens.fr/$\sim$pouzet/bib/bib.html}},
  url = {cmcs98.ps.gz},
  url = {coiteration-report98.ps.gz}
}
@techreport{lucy:verimag97,
  author = {Paul Caspi and Marc Pouzet},
  title = {{A Co-iterative Characterization of 
                  Synchronous Stream Functions}},
  institution = {VERIMAG},
  year = 1997,
  number = 07,
  month = {October},
  url = {coiteration-report98.ps.gz}
}
@inproceedings{lucy:jfla99,
  author = {Paul Caspi and Marc Pouzet},
  title = {{Lucid Synchrone: une extension fonctionnelle de Lustre}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 1999,
  address = {Morzine-Avoriaz},
  month = {F\'evrier},
  publisher = {INRIA},
  url = {jfla99.ps.gz}
}
@inproceedings{lucy:jfla99-2,
  author = {Gr\'egoire Hamon and Marc Pouzet},
  title = {{Un Simulateur Synchrone pour Lucid Synchrone}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 1999,
  address = {Morzine-Avoriaz},
  month = {F\'evrier},
  publisher = {INRIA},
  url = {jfla99-2.ps.gz}
}
@misc{lucy:genie00,
  author = {Jean-Louis Cola\c{c}o et Marc Pouzet},
  title = {{Prototypages}},
  howpublished = {Rapport final du projet GENIE II, Verilog SA},
  month = {Janvier},
  year = 2000
}
@manual{lucy:manual99,
  title = {{Lucid Synchrone, version 1.01. Tutorial and
                  reference manual}},
  author = {Paul Caspi and Marc Pouzet},
  organization = {Laboratoire d'Informatique de Paris 6},
  month = {January},
  year = 1999
}
@manual{lucy:manual01,
  author = {Marc Pouzet},
  title = {{Lucid Synchrone}, version 2.
                  {Tutorial and reference manual}},
  organization = {Universit\'e Pierre et Marie Curie, LIP6},
  month = {Mai},
  year = 2001,
  note = {Distribution available at: 
                  {\tt www.lri.fr/$\sim$pouzet/lucid-synchrone}}
}
@manual{lucy:manual06,
  author = {Marc Pouzet},
  title = {{Lucid Synchrone}, version 3.
                  {Tutorial and reference manual}},
  organization = {Universit\'e Paris-Sud, LRI},
  month = {April},
  year = 2006,
  note = {Distribution available at: 
                  \url{https://www.di.ens.fr/~pouzet/lucid-synchrone/}}
}
@techreport{lucy:lip6-00,
  author = {Paul Caspi and Marc Pouzet},
  title = {{Lucid Synchrone}, a functional extension of {Lustre}},
  institution = {Universit\'e Pierre et Marie Curie, Laboratoire LIP6},
  year = 2000
}
@unpublished{lucy:toplas,
  author = {Paul Caspi and Marc Pouzet},
  title = {{Lucid Synchrone}, a functional extension of {Lustre}},
  note = {Submitted to publication},
  year = 2002
}
@inproceedings{lucy:ppdp00,
  author = {Gr\'egoire Hamon and Marc Pouzet},
  title = {{Modular Resetting of Synchronous Data-flow Programs}},
  booktitle = {ACM International conference on
		  Principles of Declarative Programming (PPDP'00)},
  year = 2000,
  address = {Montreal, Canada},
  month = {September},
  url = {ppdp00.ps.gz},
  abstract = { This paper presents an extension
  of a synchronous data-flow 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
  data-flow 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 higher-order. 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 Mode-automata. All the experiments presented
  in the paper has been done with Lucid Synchrone, an ML extension of
  Lustre.}
}
@inproceedings{lucy:esop01,
  author = {Pascal Cuoq and Marc Pouzet},
  title = {{Modular Causality in a Synchronous Stream Language}},
  booktitle = {European Symposium on Programming (ESOP'01)},
  year = 2001,
  address = {Genova, Italy},
  month = {April},
  url = {esop01.ps.gz},
  abstract = {This article
  presents a causality analysis for a synchronous stream
  language with higher-order functions.  This analysis takes the shape
  of a type system with rows. Rows were \hbox{originally} designed to add
  extensible records to the ML type system (Didier R\'emy, Mitchell
  Wand).  We \hbox{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.}
}
@inproceedings{lucy:lpar01,
  author = {Sylvain Boulm\'e and Gr\'egoire Hamon},
  title = {{Certifying Synchrony for Free}},
  booktitle = {International Conference on Logic for Programming, Artificial                  Intelligence and Reasoning (LPAR)},
  year = 2001,
  volume = 2250,
  address = {La Havana, Cuba},
  month = {December},
  publisher = {Lecture Notes in Artificial Intelligence, Springer-Verlag},
  note = {Short version of {\em A clocked denotational semantics for
                 {L}ucid-{S}ynchrone in {C}oq}, available as a Technical 
                 Report (LIP6), at 
                 {\tt www.di.ens.fr/$\sim$pouzet/bib/bib.html}},
  url = {lpar01.ps.gz},
  url = {lucid_in_coq_report.ps.gz},
  abstract = {We express reactive programs in Coq using data-flow synchronous
operators.  Following Lucid Synchrone approach, synchro\-nous static
constraints are here expressed using dependent types. Hence, our
analysis of synchrony is here directly performed by Coq typechecker.}
}
@inproceedings{lucy:slap02,
  author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
  title = {{Type-based Initialization Analysis of a 
                   Synchronous Data-flow Language}},
  booktitle = {{Synchronous Languages, Applications, 
                  and Programming}},
  publisher = {Electronic Notes in Theoretical Computer Science},
  volume = 65,
  year = 2002,
  url = {slap02.ps.gz},
  abstract = {One of the appreciated features of the synchronous data-flow
                  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
                  data-flow program is really deterministic 
                  only if it can be shown that
                  such undefined values do not affect the 
                  behavior of the system.

                  This paper presents an {\em initialization analysis} 
                  that guarantees
                  the deterministic behavior of programs.
                  This property being undecidable in general, the paper
                  proposes a safe approximation of the property,
                  precise enough for  
                  most data-flow programs.  This analysis is a 
                  {\em one-bit} analysis --- expressions are either
                  initialized or 
                  uninitialized --- and is defined as an inference type
                  system with sub-typing constraints. This analysis
                  has been implemented 
                  in the Lucid Synchrone~compiler and in a new Scade-Lustre
                  prototype compiler. 
                  It gives very good results in practice.}
}
@inproceedings{lucy:hamon-slap04,
  author = {Gr\'egoire Hamon},
  title = {{Synchronous Data-flow Pattern Matching}},
  booktitle = {{Synchronous Languages, Applications, 
                  and Programming}},
  publisher = {Electronic Notes in Theoretical Computer Science},
  year = 2004,
  url = {hamon-slap04.ps.gz}
}
@phdthesis{lucy:these-hamon02,
  author = {Gr\'egoire Hamon},
  title = {{Calcul d'horloge et Structures de Contr\^ole
                  dans Lucid Synchrone, un langage de flots synchrones
                  \`a la ML}},
  school = {Universit\'e Pierre et Marie Curie},
  year = 2002,
  address = {Paris, France},
  month = {14 novembre}
}
@phdthesis{lucy:these-cuoq02,
  author = {Pascal Cuoq},
  title = {{Ajout de synchronisme dans les langages
                   fonctionnels typ\'es}},
  school = {Universit\'e Pierre et Marie Curie},
  year = 2002,
  address = {Paris, France},
  month = {october}
}
@manual{lucy:habilitation-pouzet02,
  author = {Marc Pouzet},
  title = {{Lucid Synchrone}: un langage synchrone d'ordre
                  sup\'erieur},
  organisation = {Universit\'e Pierre et Marie Curie},
  year = 2002,
  address = {Paris, France},
  month = {14 novembre},
  note = {Habilitation \`a diriger les recherches },
  url = {habilitation-pouzet02.ps.gz}
}
@inproceedings{lucy:emsoft03,
  author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
  title = {{Clocks as First Class Abstract Types}},
  booktitle = {Third International Conference on 
                  Embedded Software (EMSOFT'03)},
  address = {Philadelphia, Pennsylvania, USA},
  month = {october},
  year = 2003,
  url = {emsoft03.ps.gz},
  abstract = {Clocks in synchronous data-flow 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 {\em dependent types}, 
            the paper presents a simpler clock calculus reminiscent to ML type 
            systems with first order abstract types {\em \`a 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.}
}
@inproceedings{lucy:emsoft04,
  author = {Jean-Louis Cola\c{c}o and
    Alain Girault and Gr\'egoire Hamon and Marc Pouzet},
  title = {{Towards a Higher-order Synchronous Data-flow Language}},
  booktitle = {ACM Fourth International
    Conference on Embedded Software (EMSOFT'04)},
  address = {Pisa, Italy},
  month = {september},
  year = 2004,
  url = {emsoft04.pdf},
  abstract = {The paper introduces a higher-order synchronous
data-flow language in which communication channels may themselves
transport programs. This provides a mean to dynamically reconfigure
data-flow 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 first-order 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 higher-order synchronous data-flow
language where stream functions are first class citizens.}
}
@article{lucy:sttt04,
  author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
  title = {{Type-based Initialization Analysis of a 
                   Synchronous Data-flow Language}},
  journal = {International Journal on Software Tools
                  for Technology Transfer (STTT)},
  year = {2004},
  month = {August},
  volume = {6},
  number = {3},
  pages = {245--255},
  url = {sttt04.pdf}
}
@unpublished{lucy:jfp05,
  author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
  title = {{Clocks as First Class Abstract Types}},
  note = {Submitted to the Journal of Functional Programming (JFP)},
  year = 2005
}
@article{lucy:tecs06,
  author = {Alain Girault and Xavier Nicollin and Marc Pouzet},
  title = {{Automatic Rate Desynchronization of Embedded Reactive Programs}},
  journal = {ACM Transactions on Embedded Computing Systems (TECS)},
  volume = 5,
  number = 3,
  year = 2006
}
@inproceedings{lucy:emsoft05a,
  author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
                  and Claire Pagetti and Florence Plateau and Marc Pouzet},
  title = {{Synchroning Periodic Clocks}},
  booktitle = {ACM International Conference on 
                  Embedded Software (EMSOFT'05)},
  address = {Jersey city, New Jersey, USA},
  month = {September},
  year = 2005,
  url = {emsoft05a.pdf}
}
@inproceedings{lucy:emsoft05b,
  author = {Jean-Louis Cola\c{c}o and Bruno Pagano and Marc Pouzet},
  title = {{A Conservative Extension of Synchronous Data-flow with
                   State Machines}},
  booktitle = {ACM International Conference on 
                  Embedded Software (EMSOFT'05)},
  address = {Jersey city, New Jersey, USA},
  month = {September},
  year = 2005,
  url = {emsoft05b.pdf},
  abstract = {This paper presents an extension of a synchronous
data-flow language such as Lustre with imperative features expressed
in terms of powerful state machine \`a 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.

From a syntactical point of view this extension consists in
hierarchical state machines that may carry at each hierarchy level a
bunch of equations.  This proposition is an alternative to the joint
use of Simulink and Stateflow but improves it by allowing a fine
grain mix of both styles.

The central idea of the paper is to base this extension on the use of
clocks, translating imperative constructs into well clocked
data-flow programs from the basic language. This clock directed
approach is an easy way to define a semantics for the extension, it is
light to implement in an existing compiler and experiments show that
the generated code compete favorably with ad-hoc techniques.
The proposed extension has been implemented in the ReLuC compiler of
Scade/Lustre and in the Lucid Synchrone compiler.
}
}
@inproceedings{lucy:popl06,
  author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
                  and Claire Pagetti and Florence Plateau and Marc Pouzet},
  title = {{$N$-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems}},
  booktitle = {ACM International Conference on 
                  Principles of Programming Languages (POPL'06)},
  address = {Charleston, South Carolina, USA},
  month = {January},
  year = 2006,
  url = {popl06.pdf},
  abstract = { The design of high-performance stream-processing 
systems is a fast
growing domain, driven by markets such like high-end 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, real-time control
experts and computer architects, and incurs a very high level of
quality insurance and optimization.

In search for improved productivity, we propose a programming model
and language dedicated to high-performance stream processing. This
language builds on the synchronous programming model and on domain
knowledge --- the periodic evolution of streams --- to allow
correct-by-construction properties to be proven by the compiler. These
properties include resource requirements and delays between input and
output streams. Automating this task avoids tedious and error-prone
engineering, due to the combinatorics of the composition of filters
with multiple data rates and formats. Correctness of the
implementation is also difficult to assess with traditional
(asynchronous, simulation-based) approaches. This language is thus
provided with a relaxed notion of synchronous composition, called
$n$-\emph{synchrony}: two processes are $n$-synchronous if they can
communicate in the ordinary ($0$-)synchronous model with a FIFO buffer
of size $n$.

Technically, we extend a core synchronous data-flow language with a
notion of periodic clocks, and design a relaxed clock calculus (a type
system for clocks) to allow non strictly synchronous processes to be
composed or correlated. This relaxation is associated with two
sub-typing rules in the clock calculus. Delay, buffer insertion and
control code for these buffers are automatically inferred from the
clock types through a systematic transformation into a standard
synchronous program. We formally define the semantics of the language
and prove the soundness and completeness of its clock calculus and
synchronization transformation. Finally, the language is compared with
existing formalisms.}
}
@inbook{lucy:hermes06,
  author = {Paul Caspi and Gr\'egoire Hamon and Marc Pouzet},
  editor = {Nicolas Navet},
  title = {{Syst\`emes Temps-r\'eel~: Techniques de Description et 
                  de V\'erification -- Th\'eorie et Outils}},
  chapter = {{Lucid Synchrone, un langage de programmation des 
                  syst\`emes r\'eactifs}},
  publisher = {Hermes},
  volume = {1},
  year = 2006,
  pages = {217-260},
  url = {chap_lucid_synchrone_hermes06.pdf},
  abstract = {Ce chapitre pr\'esente {\bf Lucid Synchrone},
un langage d\'edi\'e \`a
la programmation de syst\`emes r\'eactifs. Il est fond\'e sur le
mod\`ele synchrone de {\bf Lustre} qu'il \'etend avec
des caract\'eristiques pr\'esentes dans les langages fonctionnels tels
que l'ordre sup\'erieur ou l'inf\'erence des types. Il offre un
m\'ecanisme de synth\`ese automatique des horloges et permet de
d\'ecrire, dans un cadre unifi\'e, une programmation flot de donn\'ees
et une programmation par automates.

Ce chapitre est une pr\'esentation du langage, destin\'ee \`a la fois au
programmeur cherchant \`a se familiariser avec celui-ci, mais aussi au
chercheur s'int\'eressant aux syst\`emes r\'eactifs et aux techniques qui
peuvent \^etre appliqu\'ees au niveau d'un langage, pour faciliter les
activit\'es de sp\'ecification, de programmation et de v\'erification.
}
}
@inproceedings{lucy:emsoft06,
  author = {Jean-Louis Cola\c{c}o and Gr\'egoire Hamon and Marc Pouzet},
  title = {{Mixing Signals and Modes in Synchronous 
                   Data-flow Systems}},
  booktitle = {ACM International Conference on 
                  Embedded Software (EMSOFT'06)},
  address = {Seoul, South Korea},
  month = {October},
  year = 2006,
  url = {emsoft06.pdf},
  abstract = {
  Synchronous data-flow languages such as SCADE/Lustre manage
  infinite sequences or {\em streams} as primitive values making them
  naturally adapted to the description of data-dominated systems.
  Their conservative extension with means to define control-structures
  or {\em modes} have been a long-term research topic and several
  solutions have emerged.

  In this paper, we pursue this effort and generalize existing
  solutions by providing two constructs: a general form of state
  machines called {\em parameterized state machines}, and valued
  signals, as can be found in Esterel. Parameterized state machines
  greatly reduce the reliance on error-prone mechanisms such as shared
  memory in automaton-based programming. Signals provide a new way of
  programming with multi-rate data in synchronous data-flow
  languages. Together, they allow for a much more direct and natural
  programming of systems that combine data-flow and state-machines.

  The proposed extension is fully implemented in the new Lucid
  Synchrone compiler.  }
}
@inproceedings{labbe07,
  author = {S\'ebastien Labb\'e and Jean-Pierre Gallois and
                  Marc Pouzet},
  title = {Slicing Communicating Automata Specifications 
                  For Efficient Model Reduction},
  booktitle = {18th Australian Conference on Software Engineering (ASWEC)},
  year = 2007
}
@inbook{lucy:iste07,
  author = {Paul Caspi and Gr\'egoire Hamon and Marc Pouzet},
  title = {Real-Time Systems: Models and verification --- Theory 
                  and tools},
  chapter = {{Synchronous Functional Programming with Lucid Synchrone}},
  publisher = {ISTE},
  year = 2007,
  editors = {Nicolas Navet and Stephan Mertz},
  url = {chap_lucid_synchrone_english_iste08.pdf},
  abstract = {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 higher-order
or constructed data-types.
The language is equipped with several static analysis, all expressed
as special type-systems and used to ensure the absence of certain
run-time errors on the final application.  It provides, in particular,
automatic type and clock inference and statically detects
initialization issues or dead-locks.
Finally, the language offers both data-flow and automata-based
programming inside a unique framework.}
}
@misc{lucy:caspicolacopouzet07,
  author = {Paul Caspi and Jean-Louis Cola\c{c}o and Marc Pouzet},
  title = {{Objects in Block-Diagram Languages}},
  month = {January},
  year = 2008,
  note = {Unpublished}
}
@inproceedings{lucy:apges07,
  author = {Darek Biernacki and Jean-Louis Colaco and Marc Pouzet},
  title = {{Clock-directed Modular Compilation from 
                   Synchronous Block-diagrams}},
  booktitle = {Workshop on Automatic Program Generation for Embedded 
                  Systems (APGES)},
  year = 2007,
  address = {Salzburg, Austria},
  month = {october},
  note = {Embedded System Week},
  url = {apges07.pdf}
}
@inproceedings{lucy:lctes08b,
  author = {Gwenael Delaval and Alain Girault and Marc Pouzet},
  title = {{A Type System for the Automatic Distribution
                   of Higher-order Synchronous Dataflow Programs}},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems 
                  (LCTES)},
  year = 2008,
  address = {Tucson, Arizona},
  month = {June},
  url = {lctes08b.pdf},
  abstract = {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 non-annotated values by means of type inference and
  to ensure, at compilation time, the consistency of the
  distribution. Our third contribution is to provide a type-directed
  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 data-flow programming language.
}
}
@inproceedings{lucy:lctes08a,
  author = {Darek Biernacki and Jean-Louis Colaco and Gr\'egoire Hamon
                  and Marc Pouzet},
  title = {{Clock-directed Modular Code Generation of Synchronous Data-flow
                   Languages}},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems 
                  (LCTES)},
  year = 2008,
  address = {Tucson, Arizona},
  month = {June},
  url = {lctes08a.pdf},
  abstract = {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 long-term
goal to develop a mathematically certified compiler for a synchronous
language as well as in simplifying existing implementations.

This article presents in full detail the modular compilation of
synchronous block diagrams into sequential code. We consider a
first-order functional language reminiscent of Lustre, which it
extends with a general n-ary merge operator, a reset
construct, and a richer notion of clocks. The clocks are used to
express activation of computations in the program and are specifically
taken into account during the compilation process to produce efficient
imperative code. We introduce a generic machine-based intermediate
language to represent transition functions, and we present a concise
clock-directed translation from the source to this intermediate
language. We address the target code generation phase by describing a
translation from the intermediate language to Java and C.
}
}
@inproceedings{lucy:aplas08,
  author = {Albert Cohen and Louis Mandel and Florence Plateau and
                  Marc Pouzet},
  title = {{Abstraction of Clocks in Synchronous Data-flow Systems}},
  booktitle = {The Sixth ASIAN Symposium on Programming Languages and Systems
              (APLAS)},
  year = 2008,
  month = {December},
  date = {9--11},
  address = {Bangalore, India},
  abstract = {Synchronous data-flow 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 so-called
  clock-calculus --- 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
  sub-typing. 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 real-time embedded software such as bounded jitter as found in
  video-systems,  execution time of real-time processes and
  scheduling resources or the communication through buffers. We
  present the algebra of clock envelopes and its main theoretical
  properties.},
  url = {aplas08.pdf},
  x-type = {article},
  topics = {team}
}
@misc{lucy:hfl09,
  author = {Albert Cohen and Louis Mandel and Florence Plateau
                  and Marc Pouzet},
  title = {{Relaxing Synchronous Composition with Clock Abstraction}},
  howpublished = {Workshop on Hardware Design using Functional languages 
                  (HFL 09) - ETAPS},
  year = 2009,
  address = {York, UK},
  url = {http://www.lri.fr/~plateau/hfl09/},
  topics = {team}
}
@inproceedings{lucy:lctes09,
  author = {Paul Caspi and Jean-Louis Cola\c{c}o and L\'eonard G\'erard
                  and Marc Pouzet and Pascal Raymond},
  title = {{Synchronous Objects with Scheduling Policies}: 
                   Introducing Safe Shared Memory in {Lustre}},
  year = {2009},
  month = {June},
  address = {Dublin},
  booktitle = {ACM International Conference on
                  Languages, Compilers, and Tools for Embedded Systems 
                  (LCTES)},
  abstract = {This paper addresses the problem of designing and implementing
  complex control systems for real-time embedded software. Typical
  applications involve different control laws corresponding to
  different phases or modes, e.g., take-off, full flight and
  landing in a fly-by-wire 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.

  In this paper, we introduce a conservative extension of a
  synchronous data-flow language close to Lustre, in order to be able
  to define systems with modes in a more modular way, while insuring
  the absence of data-races. We show that such a system can be viewed
  as an object where modes are methods acting on a shared
  memory. The object is associated to a scheduling policy which
  specifies the ways methods can be called to build a valid
  synchronous reaction. We show that the verification of the proper
  use of an object reduces to a
  type inference problem using row types introduced by Wand,
  R\'emy and Vouillon. We define the semantics of the extended
  synchronous language and the type system.
  The proposed extension has been implemented and we illustrate its
  use through several examples.},
  url = {lctes09.pdf},
  x-type = {article},
  topics = {team}
}
@inproceedings{lucy:emsoft09,
  author = {Marc Pouzet and Pascal Raymond},
  title = {{Modular Static Scheduling of Synchronous Data-flow
                  Networks: An efficient symbolic representation}},
  booktitle = {ACM International Conference on 
                  Embedded Software (EMSOFT'09)},
  address = {Grenoble, France},
  month = {October},
  year = 2009,
  url = {emsoft09.pdf},
  x-type = {article},
  topics = {team},
  abstract = {This paper addresses the question of producing modular sequential
  imperative code from synchronous data-flow 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 NP-complete.  Then, the
  authors derive an iterative algorithm looking for
  solutions for $c = 1,2,...$ where each step is encoded as a SAT
  problem.

  Despite the apparent intractability of the problem, our experience
  is that real programs do not exhibit such a complexity.
  Based on earlier work by Raymond, this paper presents a new symbolic encoding
  of the problem in terms of input/output relations. This encoding
  simplifies the problem, in the sense that it rejects
  solutions, while keeping all the optimal ones. It allows, in
  polynomial time, (1) to identify nodes for which several schedules
  are feasible and thus are possible sources of combinatorial
  explosion; (2) to obtain solutions which in some cases are already
  optimal; (3) otherwise, to get a non trivial lower bound for $c$ to
  start an iterative combinatorial search.

 The solution applies to a large class of
  block-diagram formalisms based on atomic computations and a 
    delay operator, ranging from synchronous languages such as
  Lustre or SCADE to modeling tools such as Simulink.}
}
@article{lucy:jdaes10,
  author = {Marc Pouzet and Pascal Raymond},
  title = {{Modular Static Scheduling of Synchronous Data-flow
                  Networks: An efficient symbolic representation}},
  journal = {Journal of Design Automation for Embedded Systems},
  year = 2010,
  note = {Special issue of selected papers from 
                  \url{http://esweek09.inrialpes.fr/}{Embedded System Week}.
                  Extended version of~\cite{lucy:emsoft09}.},
  volume = {3},
  number = {14},
  pages = {165-192},
  pdf = {jdaes10.pdf},
  url = {http://www.springerlink.com/content/0929-5585/14/3/},
  abstract = {This paper addresses the question of producing modular
                  sequential imperative code from synchronous
                  data-flow 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 NP-complete. Then, the
                  authors derive an iterative algorithm looking for
                  solutions for $c = 1, 2,...$ where each step is
                  encoded as a satisfiability (SAT) problem.

                  Despite the apparent intractability of the problem, our
                  experience is that real programs do not exhibit such
                  a complexity. Based on earlier work by Raymond, the
                  current paper presents a new encoding of the problem
                  in terms of input/output relations. This encoding
                  simplifies the problem, in the sense that it rejects
                  some solutions, while keeping all the optimal
                  ones. It allows, in polynomial time, (1) to identify
                  nodes for which several schedules are feasible and
                  thus are possible sources of combinatorial
                  explosion; (2) to obtain solutions which in some
                  cases are already optimal; (3) otherwise, to get a
                  non trivial lower bound for c to start an iterative
                  combinatorial search. The method has been validated
                  on several industrial examples.}
}
@misc{lucy:dcc10,
  author = {Louis Mandel and Florence Plateau
                  and Marc Pouzet},
  title = {{Lucy-n: a n-Synchronous Extension of Lustre}},
  howpublished = {Workshop on Designing Correct Circuits 
                  (DCC 10) - ETAPS},
  year = 2010,
  month = {March},
  address = {Paphos, Cyprus}
}
@article{lucy:tecs09,
  author = {C\'edric Auger and Jean-Louis Cola\c{c}o and Xun Gong
                  and Gr\'egoire Hamon and Marc Pouzet},
  title = {{From Lustre to Sequential Code: A Formalization}},
  journal = {Submitted to ACM TECS},
  year = 2009
}
@phdthesis{lucy:these-delaval08,
  author = {Gw\"enael Delaval},
  title = {{R\'epartition modulaire de programmes synchrones}},
  school = {Institut Polytechnique de Grenoble},
  year = 2008,
  address = {Grenoble, France},
  month = {1er juillet}
}
@phdthesis{lucy:these-plateau10,
  author = {Florence Plateau},
  title = {{Mod\`ele n-synchrone pour la programmation de r\'eseaux de Kahn
                   \`a m\'emoire born\'ee}},
  school = {Universit\'e Paris-Sud~11},
  year = 2010,
  address = {Orsay, France},
  month = {6 janvier},
  url = {www.lri.fr/~plateau}
}
@inproceedings{lucy:jfla10,
  author = {Louis Mandel and Florence Plateau
                  and Marc Pouzet},
  title = {{Lucy-n: une extension n-Synchrone de Lustre}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 2010,
  address = {La Ciota, France},
  month = {Janvier},
  organization = {INRIA}
}
@inproceedings{lucy:cdc10,
  author = {Albert Benveniste and Benoit Caillaud and Marc Pouzet},
  title = {{The Fundamentals of Hybrid Systems Modelers}},
  booktitle = {49th IEEE International Conference on Decision and Control (CDC)},
  year = {2010},
  address = {Atlanta, Georgia, USA},
  month = {December 15-17},
  url = {cdc10.pdf},
  abstract = { 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.

 In
 this paper we propose using \emph{non standard analysis} as a
 semantic domain for hybrid systems --- non standard analysis is an
 extension of classical analysis in which infinitesimals (the
 $\varepsilon$ and $\eta$ in the celebrated generic sentence
 $\forall \varepsilon. \exists \eta \dots$ in college maths) can be
 manipulated as first class citizens. This allows us to provide a
 denotational semantics and a constructive semantics for hybrid
 systems, thus establishing simulation engines on a firm mathematical
 basis. In passing, we cleanly separate the job of the numerical
 analyst (solving differential equations) from that of the computer
 scientist (generating execution schemes).}
}
@inproceedings{lucy:mpc10,
  author = {Louis Mandel and Florence Plateau and Marc Pouzet},
  title = {{Lucy-n: a n-Synchronous Extension of Lustre}},
  booktitle = {10th International Conference on Mathematics of
               Program Construction (MPC'10)},
  month = {June},
  year = 2010,
  address = {Manoir St-Castin, Qu\'ebec, Canada},
  publisher = {Springer LNCS},
  url = {mpc10.pdf},
  abstract = {
  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 n-synchrony relaxes synchrony by allowing the
  communication through bounded buffers whose size is computed at
  compile-time.
  % 
  It is obtained by extending the clock calculus with
  a subtyping rule which defines buffering points.

  This paper presents the first implementation of the n-synchronous
  model inside a Lustre-like language called LucyN. The language
  extends Lustre with an explicit "buffer" construct whose size
  is automatically computed during the clock calculus.
  %
  This clock calculus is defined as an inference type system and is
  parametrized by the clock language and the algorithm used to solve
  subtyping constraints.  We detail here one algorithm based on the
  abstraction of clocks, an idea originally introduced
  in~\cite{lucy:aplas08}. The paper presents a simpler, yet more
  precise, clock abstraction for which the main algebraic properties have
  been proved in Coq. Finally, we illustrate the language on various
  examples including a video application.
  }
}
@inproceedings{lucy:lctes11,
  author = {Albert Benveniste and Timothy Bourke and
                  Benoit Caillaud and Marc Pouzet},
  title = {{Divide and recycle: types and compilation for a 
                   hybrid synchronous language}},
  booktitle = {ACM SIGPLAN/SIGBED Conference on Languages, 
               Compilers, Tools and Theory for Embedded Systems (LCTES'11)},
  month = {April},
  address = {Chicago, USA},
  year = 2011,
  url = {lctes11.pdf},
  abstract = {Hybrid modelers such as Simulink have become corner stones of embedded 
  systems development.
  They allow both \emph{discrete} controllers and their \emph{continuous} 
  environments to be expressed \emph{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.

  Starting from a minimal, yet full-featured, Lustre-like synchronous
  language, this paper presents a conservative extension
  where data-flow equations can be mixed with ordinary differential
  equations (ODEs) with possible reset.
  A type system is proposed to statically distinguish discrete computations 
  from continuous ones and to ensure that signals are used in their proper 
  domains.
  We propose a semantics based on \emph{non-standard analysis} which gives a 
  synchronous interpretation to the whole language, clarifies the 
  discrete/continuous interaction and the treatment of zero-crossings, and 
  also allows the correctness of the type system to be established.

  The extended data-flow language is realized through a source-to-source 
  transformation into a synchronous subset, which can then be compiled using 
  existing tools into routines that are both efficient and bounded in their 
  use of memory.
  These routines are orchestrated with a single off-the-shelf numerical 
  solver using a simple but precise algorithm which treats causally-related 
  cascades of zero-crossings.
  We have validated the viability of the approach through experiments with 
  the SUNDIALS library.},
  x-type = {article},
  topics = {team}
}
@inproceedings{lucy:emsoft11,
  author = {Albert Benveniste and Timothy Bourke and
                  Benoit Caillaud and Marc Pouzet},
  title = {{A Hybrid Synchronous Language with Hierarchical
  Automata}: {Static Typing and Translation to Synchronous Code}},
  booktitle = {ACM SIGPLAN/SIGBED Conference on Embedded Software (EMSOFT'11)},
  month = {October},
  address = {Taipei, Taiwan},
  year = 2011,
  url = {emsoft11.pdf},
  abstract = {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.

Following the approach of Benveniste et al., we present the design of
a hybrid modeler built from a synchronous language and an
off-the-shelf numerical solver.  The main novelty is a language which
includes
control structures, such as hierarchical
automata, for both continuous and discrete contexts.  These constructs
can be arbitrarily mixed with data-flow and ordinary differential
equations (ODEs).  A type system is required to statically ensure that
all discrete state changes are aligned with zero-crossing events and
that the function passed to the numerical solver is free of
side-effects during integration.
We show that well-typed programs can be compiled through a source-to-source 
translation into synchronous code which is then translated into 
sequential code using an existing synchronous language compiler.

Based on the presented material, a compiler for a new synchronous language 
with hybrid features has been developed.
We demonstrate its effectiveness on some examples.
}
}
@inproceedings{lucy:fmcad11,
  author = {Louis Mandel and Florence Plateau and Marc Pouzet},
  title = {{Static Scheduling of Latency Insensitive Designs 
                  with Lucy-n}},
  year = 2011,
  booktitle = {International Conference on
                  Formal Methods in Computer-Aided Design (FMCAD)},
  address = {Austin, Texas, USA},
  month = {October 30 -- November 2},
  abstract = {Lucy-n is a data-flow programming language similar to Lustre
  extended with a buffer operator.
  It is based on the n-synchronous model which was initially
  introduced for programming multimedia streaming applications. In
  this article, we show that Lucy-n 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 Lucy-n
  program. Then, the Lucy-n compiler automatically provides static
  schedules for computation nodes and buffer sizes needed in shell
  wrappers.},
  url = {MandelPlateauPouzet-FMCAD-2011.pdf}
}
@article{lucy:jcss12,
  author = {Albert Benveniste and Timothy Bourke and Benoit
                  Caillaud and Marc Pouzet},
  title = {{Non-Standard Semantics of Hybrid Systems Modelers}},
  journal = {Journal of Computer and System Sciences (JCSS)},
  year = 2012,
  note = {Special issue in honor of Amir Pnueli},
  doi = {http://dx.doi.org/10.1016/j.jcss.2011.08.009},
  volume = {78},
  number = {3},
  month = {May},
  pages = {877-910},
  url = {jcsspaper.pdf},
  abstract = {  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).

  In this paper we propose using techniques from \emph{non-standard
    analysis} to define a semantic domain for hybrid systems.
  Non-standard analysis is an extension of classical analysis in which
  infinitesimal (the $\varepsilon$ and $\eta$ in the celebrated
  generic sentence $\forall\varepsilon\exists\eta\dots$ of college
  maths) can be manipulated as first class citizens.  This approach
  allows us to define both a denotational semantics, a constructive
  semantics, and a Kahn Process Network semantics for hybrid systems,
  thus establishing simulation engines on a sound but flexible
  mathematical foundation.  These semantics offer a clear distinction
  between the concerns of the numerical analyst (solving differential
  equations) and those of the computer scientist (generating execution
  schemes).

  We also discuss a number of practical and fundamental issues in
  hybrid system modelers that give rise to non reproducibility of
  results, nondeterminism, and undesirable side effects. Of particular
  importance are cascaded mode changes (also called ``zero-crossings''
  in the context of hybrid systems modelers).}
}
@inproceedings{lucy:lctes12,
  author = {L\'eonard G\'erard and Adrien Guatto and
                  C\'edric Pasteur and Marc Pouzet},
  title = {{A Modular Memory Optimization for Synchronous Data-Flow 
                   Languages. Application to Arrays in a Lustre Compiler}},
  booktitle = {Languages, Compilers and Tools for Embedded Systems
                  (LCTES'12)},
  year = 2012,
  address = {Beijing},
  month = {June 12-13},
  organization = {ACM},
  abstract = {The generation of efficient sequential code for
synchronous data-flow 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.

  This article presents a two-levels solution to the memory
  optimization problem. It combines a compile-time optimization
  algorithm, reminiscent of register allocation, paired with language
  annotations on the source given by the designer. Annotations
  express in-place modifications and control where allocation is performed.
  Moreover, they allow external functions
  performing \emph{in-place} modifications to be imported safely. Soundness of
  annotations is guaranteed by a semilinear type system and additional
  scheduling constraints. A key feature is that annotations
  for well-typed programs do not change the semantics of the language:
  removing them may lead to a less efficient code
  but with the very same semantics.

  The method has been implemented in a new compiler for a Lustre-like
  synchronous language extended with hierarchical automata and arrays.
    Experiments show that the proposed approach removes most of the
  unnecessary array copies, resulting in faster code that
  uses less memory.},
  note = {Best paper award},
  url = {lctes12.pdf}
}
@inproceedings{lucy:emsoft12,
  author = {Albert Cohen and L\'eonard G\'erard and Marc Pouzet},
  title = {{Programming parallelism with futures in Lustre}},
  booktitle = {ACM International Conference on Embedded Software (EMSOFT'12)},
  year = 2012,
  address = {Tampere, Finland},
  organization = {ACM},
  month = {October 7-12},
  abstract = {Efficiently distributing synchronous programs is a challenging and
  long-standing subject. This paper introduces the use
  of \emph{futures} in a Lustre-like 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.

  Through a number of examples, we show how to desynchronize long
  computations and implement parallel patterns such as fork-join,
  pipelining and data parallelism.  The proposed extension preserves
  the main static properties of the base language, including
  static resource bounds and the absence of deadlock, livelock and
  races.  Moreover, we prove that adding or removing futures preserves
  the underlying synchronous semantics.},
  note = {Best paper award},
  url = {emsoft12.pdf}
}
@inproceedings{lucy:hscc13,
  author = {Timothy Bourke and Marc Pouzet},
  title = {{Z\'elus, a Synchronous Language with ODEs}},
  booktitle = {International Conference on
                  Hybrid Systems: Computation and Control (HSCC 2013)},
  year = 2013,
  month = {April 8--11},
  address = {Philadelphia, USA},
  organization = {ACM},
  abstract = {
Z\'elus 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 Lustre-like synchronous language with Ordinary
Differential Equations (ODEs). The extension is conservative: any 
synchronous program expressed as data-flow equations and hierarchical 
automata can be composed arbitrarily with ODEs in \emph{the same source 
code}.

A dedicated type system and causality analysis ensure that all discrete 
changes are aligned with
zero-crossing events so that no side effects or discontinuities occur
during integration. Programs are statically
scheduled and translated into sequential code which, by construction, runs 
in bounded time and space.
Compilation is effected by source-to-source translation into a small 
synchronous subset which is
processed by a standard synchronous compiler architecture.
The resulting code is paired with an off-the-shelf numeric solver.

This experiment show that it is possible to build a modeler for
explicit hybrid systems \emph{\`a la Simulink/Stateflow} on top of an
existing synchronous language, using it both as a semantic basis and as a
target for code generation.},
  url = {hscc13.pdf}
}
@manual{lucy:zelus-web,
  author = {Timothy Bourke and Marc Pouzet},
  title = {{Z\'elus}, a Synchronous Language with ODEs},
  organization = {\'Ecole normale sup\'erieure},
  month = {June},
  year = 2013,
  note = {{\tt {www.di.ens.fr/zelus}}}
}
@inproceedings{lucy:hscc14,
  author = {Albert Benveniste and Timothy Bourke and Benoit
                  Caillaud and Bruno Pagano and Marc Pouzet},
  title = {{A Type-based Analysis of Causality Loops in Hybrid
                  Systems Modelers}},
  booktitle = {International Conference on
               Hybrid Systems: Computation and Control (HSCC)},
  year = 2014,
  month = {April 15--17},
  address = {Berlin, Germany},
  organization = {ACM},
  abstract = {Explicit hybrid systems modelers like Simulink/Stateflow allow
for programming both discrete- and continuous-time behaviors with
complex interactions between them.  A key issue in their compilation is the static
detection of algebraic or \emph{causality} loops.  Such loops can
cause simulations to deadlock
%, are a source of compilation bugs
and prevent the generation of statically scheduled code.

This paper addresses this issue for a hybrid modeling language that
combines synchronous Lustre-like data-flow equations with Ordinary
Differential Equations (ODEs).  We introduce the operator \emph{last(x)}
for the left-limit of a signal \emph{x}.  This operator is used to break
causality loops and permits a uniform treatment of discrete and
continuous state variables. The semantics relies on non-standard
analysis, defining an execution as a sequence of infinitesimally small
steps.  A signal is deemed \emph{causally correct} when it can be
computed sequentially and only progresses by infinitesimal steps
outside of discrete events.  The causality analysis takes the form of
a simple type system. In well-typed programs, signals are proved continuous
during integration.

The effectiveness of this system is illustrated with several examples
written in Z\'elus, a Lustre-like synchronous language extended with
hierarchical automata and ODEs.},
  url = {hscc14.pdf}
}
@manual{zelus:distribution13,
  author = {Timothy Bourke and Marc Pouzet},
  title = {Z\'elus, a Hybrid Synchronous Language},
  organization = {\'Ecole normale sup\'erieure},
  month = {September},
  year = 2013,
  note = {Distribution at: {\tt zelus.di.ens.fr}},
  url = {http://zelus.di.ens.fr}
}
@manual{zelus:sundialsML13,
  author = {Timothy Bourke and Marc Pouzet},
  title = {{SundialsML: an ML binding for Sundials CVODE}},
  organization = {\'Ecole normale sup\'erieure},
  month = {September},
  year = 2013,
  note = {Distribution at: {\tt zelus.di.ens.fr}},
  url = {http://zelus.di.ens.fr}
}
@inproceedings{lucy:cc2015,
  author = {Timothy Bourke and Jean-Louis Cola\c{c}o and Bruno Pagano and
                  C\'edric Pasteur and Marc Pouzet},
  title = {{A Synchronous-based Code Generator For Explicit
                  Hybrid Systems Languages}},
  booktitle = {International Conference on Compiler Construction (CC)},
  month = {April 11-18},
  address = {London, UK},
  series = {LNCS},
  organisation = {ETAPS},
  year = 2015,
  abstract = {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.

This paper presents a novel approach for generating code from a hybrid
systems modeling language. By building on top of an existing
synchronous language and compiler, it reuses almost all the existing
infrastructure with only a few modifications.  Starting from an
existing synchronous data-flow language conservatively extended with
Ordinary Differential Equations (ODEs), this paper details the
sequence of source-to-source transformations that ultimately yield
sequential code.  A generic intermediate language is introduced to
represent transition functions.
The versatility of this approach is exhibited by treating two classical 
simulation targets:
code that complies with the FMI standard
and code directly linked with an off-the-shelf numerical solver (Sundials 
CVODE).

The presented material has been implemented in the Z\'elus compiler
and the industrial KCG code generator of SCADE 6.},
  url = {cc15.pdf}
}
@inproceedings{lucy:emsoft15-talk,
  author = {Marc Pouzet},
  title = {{Building a Hybrid Systems Modeler on Synchronous
  Languages Principles}},
  booktitle = {ACM International Conference on Embedded Software (EMSOFT)},
  month = {October 4-9},
  address = {Amsterdam},
  year = 2015,
  note = {Invited talk},
  url = {emsoft15-talk.pdf}
}
@inproceedings{mixed_time_critical_ertss016,
  author = {Albert Cohen and
                  Valentin Perrelle
		  and Dumitru Potop-Butucaru
		  and Marc Pouzet
		  and Elie Soubiran
		  and Zhen Zhang},
  title = {{Hard Real Time and Mixed Time Criticality on
                   Off-The-Shelf Embedded Multi-Cores}},
  booktitle = {ERTS},
  month = {January},
  address = {Toulouse},
  year = 2016,
  abstract = {The paper describes a pragmatic solution to the parallel
                  execution of hard real-time tasks on off-the-shelf
                  embedded multiprocessors. We propose a simple
                  timing isolation protocol allowing computational
                  tasks to communicate with hard real-time
                  ones. Excellent parallel resource utilization can be
                  achieved while preserving timing
                  compositionality. An extension to a synchronous
                  language enables the correct-by-construction
                  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
                  DO-178B.},
  url = {mixed_time_critical_erts2.pdf}
}
@inproceedings{lucy:fmcad16,
  author = {Guillaume Baudart and Timothy
  Bourke and Marc Pouzet},
  title = {{Soundness of the
  Quasi-Synchronous Abstraction}},
  year = 2016,
  booktitle = {International Conference on Formal Methods in Computer-Aided Design
  (FMCAD)},
  address = {Mountain View, California, USA},
  month = {October, 3-6},
  abstract = {Many critical real-time embedded systems
  are implemented as a set of processes that execute periodically with
  bounded jitter and communicate with bounded transmission delay. The
  quasi-synchronous ab- straction was introduced by P. Caspi for
  model-checking 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 real-time model and the quasi-synchronous
  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.},
  url = {fmcad16-extended.pdf}
}
@inproceedings{lucy:jfla17,
  author = {Timothy Bourke and Pierre-\'Evariste Dagand and Marc Pouzet and Lionel Rieg},
  title = {V\'erification de la g\'en\'eration modulaire du code imp\'eratif pour Lustre
},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JLFA)},
  year = 2017,
  month = {January},
  address = {Gourette, Pyr\'en\'ees, France},
  abstract = {Les langages synchrones sont utilis\'es pour programmer
                  des logiciels de contr\^ole-commande d'applications
                  critiques. Le langage Scade, utilis\'e dans
                  l'industrie pour ces applications, est fond\'e sur le
                  langage Lustre introduit par Caspi et Halbwachs. On
                  s'int\'eresse ici \`a la formalisation et la preuve,
                  dans l'assistant de preuve Coq, d'une \'etape clef de
                  la compilation : la traduction de programmes Lustre
                  vers des programmes d'un langage imp\'eratif. Le d\'efi
                  est de passer d'une s\'emantique synchrone flot de
                  donn\'ees, o\`u un programme manipule des flots, \`a une
                  s\'emantique imp\'erative, o\`u un programme manipule la
                  m\'emoire de fa\c{c}on s\'equentielle. Nous sp\'ecifions et
                  v\'erifions un g\'en\'erateur de code simple qui g\`ere les
                  traits principaux de Lustre : l'\'echantillonnage, les
                  noeuds et les d\'elais. La preuve utilise un mod\`ele
                  s\'emantique interm\'ediaire qui m\'elange des traits flot
                  de donn\'ees et imp\'eratifs et permet de d\'efinir un
                  invariant inductif essentiel. Nous exploitons la
                  formalisation propos\'ee pour v\'erifier une
                  optimisation classique qui fusionne des structures
                  conditionnelles dans le code imp\'eratif g\'en\'er\'e.},
  url = {jfla17.pdf}
}
@article{lucy:nahs17,
  author = {Albert Benveniste and Timothy Bourke and Benoit
                  Caillaud and Bruno Pagano and Marc Pouzet},
  title = {{A Type-based Analysis of Causality Loops in Hybrid
                  Systems Modelers}},
  journal = {Journal of Nonlinear Analysis Hybrid Systems},
  year = 2017,
  note = {In press. Selected paper from HSCC'14},
  abstract = {Explicit hybrid systems modelers like
                  \emph{Simulink/Stateflow} allow for programming both
                  discrete- and continuous-time behaviors with complex
                  interactions between them.  An important step in
                  their compilation is the static detection of
                  algebraic or \emph{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 data-flow equations with
                  Ordinary Differential Equations (ODEs).  We
                  introduce the operator \emph{last(x)} for the left-limit
                  of a signal $x$.  The \emph{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
                  non-standard analysis, defining an execution as a
                  sequence of infinitesimally small steps.  A signal
                  is deemed \emph{causally correct} when it can be
                  computed sequentially and only changes
                  infinitesimally outside of announced discrete events
                  like zero-crossings.  The causality analysis takes
                  the form of a type system that expresses
                  dependencies between signals. In well-typed
                  programs, (\emph{i}) signals are \emph{provably
                  continuous during integration} provided that
                  imported external functions are also continuous, and
                  (\emph{ii}) \emph{sequential code can be generated}.
                  The effectiveness of the system is illustrated with
                  several examples written in Zelus{}, a Lustre-like
                  synchronous language extended with ODEs.}
}
@inproceedings{lucy:hscc17,
  author = {Albert Benveniste and Benoit
                  Caillaud and Hilding Elmqvist and Khalil Ghorbal and Martin Otter and Marc Pouzet},
  title = {{Structural Analysis of Multi-Mode DAE Systems}},
  booktitle = {International Conference on
               Hybrid Systems: Computation and Control (HSCC)},
  year = 2017,
  month = {April 18-20},
  address = {Pittsburgh, USA},
  organization = {ACM},
  abstract = {Differential Algebraic Equation (DAE) systems constitute
                  the mathematical model supporting physical modeling
                  languages such as Modelica, VHDL-AMS, or
                  Simscape. Unlike ODEs, they exhibit subtle issues
                  because of their implicit latent equations and
                  related differentiation index. Multi-mode DAE (mDAE)
                  systems are much harder to deal with, not only
                  because of their mode-dependent 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 multi-mode 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.},
  url = {hscc17.pdf}
}
@inproceedings{lucy:pldi17,
  author = {Timothy Bourke and L\'elio Brun and Pierre-\'Evariste Dagand and Xavier Leroy and Marc Pouzet and Lionel Rieg},
  title = {{A Formally Verified Compiler for Lustre}},
  booktitle = {International Conference on Programming Language, Design and
                  Implementation (PLDI)},
  year = 2017,
  month = {June 19-21},
  address = {Barcelona, Spain},
  organization = {ACM},
  abstract = {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.},
  url = {pldi2017.pdf}
}
@inproceedings{lucy:emsoft17,
  author = {Timothy Bourke and Francois Carcenac and Jean-Louis Cola\c{c}o
                  and Bruno Pagano and C\'edric Pasteur and Marc Pouzet},
  title = {{A Synchronous Look at the Simulink Standard Library}},
  booktitle = {ACM International Conference on Embedded Software (EMSOFT)},
  month = {October 15-20},
  address = {Seoul},
  year = 2017,
  abstract = {Hybrid systems modelers like
  Simulink come with a rich collection of discrete-time and
  continuous-time blocks. Most blocks are not defined in terms of more
  elementary ones---and some cannot be---but are instead written in
  imperative code and explained informally in a reference
  manual. This raises the question of defining a minimal set of
  orthogonal programming constructs such that
  most blocks can be \emph{programmed} directly and thereby given
  a specification that is mathematically precise, and whose compiled
  version performs comparably to handwritten code.
  
  In this paper, we show that a fairly large set of blocks from the
  Simulink standard library can be programmed in a precise, purely
  functional language using stream equations, hierarchical automata,
  Ordinary Differential Equations (ODEs), and deterministic
  synchronous parallel composition.  Some blocks cannot be expressed
  as they mix discrete-time and continuous-time signals in
  unprincipled ways and so are statically forbidden by the type
  checker.

  The experiment is conducted in Z\'elus, a synchronous language that
  conservatively extends Lustre with constructs for
  programming systems that mix discrete-time and continuous-time signals.
},
  url = {emsoft17.pdf}
}
@unpublished{lucy:velus10,
  author = {C\'edric Auger and  Jean-Louis Colaco and
     Gr\'egoire Hamon and Marc Pouzet},
  title = {{A formalization and proof of a modular Lustre compiler}},
  note = {Accompaning paper of LCTES'08},
  year = 2010
}
@inproceedings{lucy:tase17,
  author = {Jean-Louis Colaco and Bruno Pagano and Marc Pouzet},
  title = {{Scade 6: A Formal Language
for Embedded Critical Software Development}},
  booktitle = {{Eleventh International Symposium on
                  Theoretical Aspect of Software Engineering (TASE)}},
  year = 2017,
  month = {September 13-15},
  address = {Sophia Antipolis, France},
  abstract = {SCADE is a high-level language and environment for
                  developing safety critical embedded control
                  software. It is used for more than twenty years in
                  various application domains like avionics, nuclear
                  plants, transportation, automotive. SCADE has been
                  founded on the synchronous data-flow language Lustre
                  invented by Caspi and Halbwachs. In the early years,
                  it was mainly seen as a graphical notation for
                  Lustre but with the unique and key addition of a
                  code generator qualified with the highest standards
                  for safety critical applications.

In 2008, a major
                  revision based on the new language `Scade 6' was
                  released. This language originally combines the
                  Lustre data-flow style with control structures
                  borrowed from Esterel and SyncCharts, compilation
                  and static analyses from Lucid Synchrone to ensure
                  safety properties. This expressiveness increase
                  for SCADE together with a qualified code generator
                  have dramatically widened the scope of applications
                  developed with.

While previous publications have
                  described some of its language constructs and
                  compiler algorithms, no reference publication on
                  `Scade 6' existed so far. In this paper, we come
                  back to the decisions made for its design,
                  illustrate the main language features, static
                  analyses, and the compiler organization in the
                  context of a qualification process.},
  url = {tase17.pdf}
}
@inproceedings{lucy:fdl17,
  author = {Guillaume Baudart and Timothy Bourke and Marc Pouzet},
  title = {{Symbolic Simulation of
Dataflow Synchronous Programs with Timers}},
  booktitle = {Forum on specification \& Design Languages (FDL)},
  year = 2017,
  month = {September 18-20},
  address = {Verona, Italy},
  abstract = {The synchronous language Lustre and its descendants
                  have long been used to program and model discrete
                  controllers. Recent work shows how to mix discrete
                  and continuous elements in a Lustre-like language
                  called Z\'élus. The resulting hybrid programs are
                  deterministic and can be simulated with a numerical
                  solver. In this article, we focus on a subset of
                  hybrid programs where continuous behaviors are
                  expressed using timers, nondeterministic guards, and
                  invariants, as in Timed Safety Automata. We propose
                  a source-to-source compilation pass to generate
                  discrete code that, coupled with standard operations
                  on Difference-Bound Matrices, produces symbolic
                  traces that each represent a set of concrete
                  traces.},
  url = {fdl17.pdf}
}
@inproceedings{aguado:esop18,
  author = {Aguado, Joaqu{\'i}n
and Mendler, Michael
and Pouzet, Marc
and Roop, Partha
and von Hanxleden, Reinhard},
  editor = {Ahmed, Amal},
  title = {Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach},
  booktitle = {27th European Symposium on Programming (ESOP)},
  year = {2018},
  publisher = {Springer International Publishing},
  address = {Thessaloniki, Greece},
  abstract = {Synchronous Programming (SP) is a universal computational
                  principle that provides deterministic
                  concurrency. The same input sequence with the same
                  timing always results in the same externally
                  observable output sequence, even if the internal
                  behaviour generates uncertainty in the scheduling of
                  concurrent memory accesses. Consequently, SP
                  languages have always been strongly founded on
                  mathematical semantics that support formal program
                  analysis. So far, however, communication has been
                  constrained to a set of primitive clock-synchronised
                  shared memory (csm) data types, such as data-flow
                  registers, streams and signals with restricted read
                  and write accesses that limit modularity and
                  behavioural abstractions.},
  url = esop_aguado_final.pdf
}
@phdthesis{lucy:these-guatto16,
  author = {Adrien Guatto},
  title = {{A Synchronous Functional Language with Integer Clocks}},
  school = {\'Ecole normale sup\'erieure},
  year = 2016,
  address = {\'Ecole normale sup\'erieure, 45 rue d'Ulm, 75230 Paris, France},
  month = {7 janvier},
  url = {https://www.irif.fr/~guatto/papers/thesis_guatto.pdf}
}
@article{lucy:ieee18,
  author = {Albert Benveniste and Timothy Bourke
                  and Beno\^{\i}t Caillaud and Jean-Louis Cola\c{c}o
                  and C\'edric Pasteur and Marc Pouzet},
  title = {{Building a Hybrid Systems Modeler on Synchronous
  Languages Principles}},
  journal = {Proceedings of the IEEE},
  year = 2018,
  abstract = { Hybrid systems modeling languages that mix discrete and
  continuous time signals and systems are widely used to develop
  Cyber-Physical systems where control software interacts with
  physical devices. Compilers play a central role, statically checking
  source models, generating intermediate representations for testing
  and verification, and producing sequential code for simulation and
  execution on target platforms.

  This paper presents a novel approach
  to the design and implementation of a hybrid systems language,
  built on synchronous language principles and their proven
  compilation techniques. The result is a hybrid systems modeling
  language in which synchronous programming constructs can be mixed
  with Ordinary Differential Equations (ODEs) and zero-crossing
  events, and a runtime that delegates their approximation to an
  off-the-shelf numerical solver.

  We propose an ideal semantics based
  on non standard analysis, which defines the execution of a hybrid
  model as an infinite sequence of infinitesimally small time
  steps. It is used to specify and prove correct three essential
  compilation steps: (1) a type system that guarantees that a
  continuous-time signal is never used where a discrete-time one is
  expected and conversely; (2) a type system that ensures the absence
  of combinatorial loops; (3) the generation of statically scheduled
  code for efficient execution.

  Our approach has been evaluated in
  two implementations: the academic language Zelus, which extends a
  language reminiscent of Lustre with ODEs and zero-crossing events,
  and the industrial prototype Scade Hybrid, a conservative extension
  of Scade 6.},
  url = ieee18.pdf
}
@inproceedings{rml:jfla19,
  author = {Guillaume Baudart and Louis Mandel and Marc Pouzet},
  title = {Programmation Synchrone aux JFLA},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JLFA)},
  year = 2019,
  month = {Janvier},
  address = {Les Rousses},
  abstract = {Depuis 1999, 39 articles et expos\'es li\'es \`a la
programmation synchrone ont \'et\'e pr\'esent\'es aux JFLA. Ces articles
couvrent de nombreux aspects qui illustrent les liens \'etroits qui
existent entre la programmation synchrone et les langages applicatifs
: conception de langages, s\'emantique, typage, compilation, ex\'ecution,
analyse de programmes, certification de compilateurs. Dans
cet article nous revenons sur quelques uns de ces r\'eesultats qui
illustrent la proximit\'e des deux domaines.},
  url = {jfla19-rml-lucy.pdf}
}
@inproceedings{velus:jfla19,
  author = {Timothy Bourke and Marc
  Pouzet},
  title = {Arguments cadenc\'es dans un compilateur Lustre
  v\'erifi\'e},
  booktitle = {Journ\'ees Francophones des Langages
  Applicatifs (JLFA)},
  year = 2019,
  month = {Janvier},
  address = {Les
  Rousses},
  abstract = {Lustre est un langage synchrone pour
  programmer des syst\`emes avec des sch\'emas-blocs desquels un code
  imp\'eratif de bas niveau est g\'en\'er\'e automatiquement. Des travaux
  r\'ecents utilisent l'assistant de preuve Coq pour sp\'ecifier un
  compilateur d'un noyau de Lustre vers le langage Clight de CompCert
  pour ensuite g\'en\'erer du code assembleur. La preuve de correction de
  l'ensemble relie la s\'emantique de flots de Lustre avec la s\'emantique
  impérative du code assembleur.  Chaque flot dans un programme Lustre
  est associé avec une ``horloge'' statique qui repr\'esente ses
  instants d'activation. La compilation transforme les horloges en des
  instructions conditionnelles qui d\'eterminent quand les valeurs
  associ\'es sont calcul\'ees. Les travaux pr\'ec\'edents faisaient
  l'hypoth\`ese simplificatrice que toutes les entr\'ees et sorties d'un
  bloc partagent la m\^eme horloge. Cet article d\'ecrit une façon de
  supprimer cette restriction. Elle exige d'abord d'enrichir les
  r\`egles de typage des horloges et le mod\`ele s\'emantique. Ensuite, pour
  satisfaire le mod\`ele s\'emantique de Clight, on ajoute une \'etape de
  compilation pour assurer que chaque variable pass\'ee directement \`a un
  appel de fonction a \'et\'e initialis\'ee.},
  url = {jfla19-velus.pdf}
}
@article{BourkeInoPou:SundialsML:2018,
  author = {Timothy Bourke
		   and Jun Inoue
		   and Marc Pouzet},
  title = {{Sundials/ML}: connecting {OCaml} to the {Sundials}
                   numeric solvers},
  publisher = {{Open Publishing Association}},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = 285,
  pages = {101--130},
  year = 2018,
  doi = {10.4204/EPTCS.285.4},
  url = {paper-sundialsmld2018.pdf},
  note = {Extended version of paper appearing in the ACM Worshop on ML, 2016},
  abstract = {This paper describes the design and implementation of a
                  comprehensive OCaml interface to the Sundials
                  library of numeric solvers for ordinary differential
                  equations, differential algebraic equations, and
                  non-linear equations. The interface provides a
                  convenient and memory-safe alternative to using
                  Sundials directly from C and facilitates application
                  development by integrating with higher-level
                  language features, like garbage-collected memory
                  management, algebraic data types, and
                  exceptions. Our benchmark results suggest that the
                  interface overhead is acceptable: the standard
                  examples are rarely twice as slow in OCaml than in
                  C, and often less than 50\% slower. The challenges
                  in interfacing with Sundials are to efficiently and
                  safely share data structures between OCaml and C, to
                  support multiple implementations of vector
                  operations and linear solvers through a common
                  interface, and to manage calls and error signalling
                  to and from OCaml. We explain how we overcame these
                  difficulties using a combination of standard
                  techniques such as phantom types and polymorphic
                  variants, and carefully crafted data
                  representations.}
}
@incollection{lucy:dae19,
  author = {Albert Benveniste and
  Benoit Caillaud and Hilding Elmquist and Khalil Ghorbal and
  Martin Otter and Marc Pouzet},
  title = {Multi-Mode DAE Models - Challenges, Theory and
                  Implementation. },
  booktitle = {Computing and Software Science: state of the Art and
                  Perspectives},
  editor = {Steffen B., Woeginger G.},
  publisher = {Springer},
  year = 2019,
  volume = 10000,
  series = {Lecture Notes in Computer Science},
  abstract = {Our objective is to model and simulate Cyber-Physical
                  Systems (CPS) such as robots, vehicles, and power
                  plants. The structure of CPS models may change
                  during simulation due to the desired operation, due
                  to failure situations or due to changes in physical
                  conditions. Corresponding models are called
                  multi-mode. We are interested in multi-domain,
                  component-oriented modeling as performed, for
                  example, with the modeling language Modelica that
                  leads naturally to Differential Algebraic Equations
                  (DAEs). This paper is thus about multi-mode DAE
                  systems. In particular, new methods are discussed to
                  overcome one key problem that was only solved for
                  specific subclasses of systems before: How to switch
                  from one mode to another one when the number of
                  equations may change and variables may exhibit
                  impulsive behavior? An evaluation is performed both
                  with the experimental modeling and simulation system
                  Modia, a domain specific language extension of the
                  programming language Julia, and with SunDAE, a novel
                  structural analysis library for multi-mode DAE
                  systems.}
}
@inproceedings{lucy:popl20,
  author = {Timothy Bourke and L\'elio Brun and Marc Pouzet},
  title = {{Mechanized Semantics and Verified Compilation
                   for a Dataflow Synchronous Language with Reset}},
  booktitle = {International Conference on Principles of
               Programming Languages (POPL)},
  year = 2020,
  month = {January 19-25},
  address = {New Orleans, Louisiana, United States},
  organization = {ACM},
  abstract = {Specifications based on block diagrams and state machines are used to design
control software, especially in the certified development of safety-critical
applications. Tools like SCADE Suite and Simulink/Stateflow are equipped
with compilers that translate such specifications into executable code. They
provide programming languages for composing functions over streams as
typified by Dataflow Synchronous Languages like Lustre.

Recent work builds on CompCert to specify and verify a compiler for the core
of Lustre in the Coq Interactive Theorem Prover. It formally links the
stream-based semantics of the source language to the sequential memory
manipulations of generated assembly code. We extend this work to treat a
primitive for resetting subsystems. Our contributions include new semantic
rules that are suitable for mechanized reasoning, a novel intermediate
language for generating optimized code, and proofs of correctness for the
associated compilation passes.},
  url = {popl20.pdf}
}
@misc{lucy:rpp19,
  title = {Reactive Probabilistic Programming},
  author = {Guillaume Baudart and Louis Mandel and
    Eric Atkinson and Benjamin Sherman and Marc Pouzet and Michael Carbin},
  year = {2019},
  eprint = {1908.07563},
  archiveprefix = {arXiv},
  primaryclass = {cs.PL},
  abstract = {Synchronous reactive languages were introduced for
                  designing and implementing real-time control
                  software. These domain-specific languages allow for
                  writing a modular and mathematically precise
                  specification of the system, enabling a user to
                  simulate, test, verify, and, finally, compile the
                  system into executable code. However, to date these
                  languages have had limited modern support for
                  modeling uncertainty -- probabilistic aspects of the
                  software's environment or behavior -- even though
                  modeling uncertainty is a primary activity when
                  designing a control system.  In this paper we extend
                  Zelus, a synchronous programming language, to
                  deliver ProbZelus, the first synchronous
                  probabilistic programming language. ProbZelus is a
                  probabilistic programming language in that it
                  provides facilities for probabilistic models and
                  inference: inferring latent model parameters from
                  data.  We present ProbZelus's measure-theoretic
                  semantics in the setting of probabilistic, stateful
                  stream functions. We then demonstrate a
                  semantics-preserving compilation strategy to a
                  first-order functional core calculus that lends
                  itself to a simple semantic presentation of
                  ProbZelus's inference algorithms. We also redesign
                  the delayed sampling inference algorithm to provide
                  bounded and streaming delayed sampling inference for
                  ProbZelus models. Together with our evaluation on
                  several reactive programs, our results demonstrate
                  that ProbZelus provides efficient, bounded memory
                  probabilistic inference.}
}
@inproceedings{lucy:jfla20,
  author = {Guillaume Baudart and Louis Mandel
  and Eric Atkinson and Benjamin Sherman  and Marc Pouzet and Michael Carbin},
  title = {{Programmation d'applications r\'eactives probabilistes}},
  year = 2020,
  month = {Janvier},
  address = {Gruissan},
  abstract = {Les langages synchrones ont \'et\'e introduits pour concevoir
                  des syst\`emes embarqu\'es temps-r\'eel.  Ces langages
                  d\'edi\'es permettent d'\'ecrire une sp\'ecification pr\'ecise
                  du syst\`eme, de la simuler, la valider par du test ou
                  de la v\'erification formelle puis de la compiler vers
                  du code ex\'ecutable.  Cependant, ils offrent un
                  support limit\'e pour mod\'eliser les comportements
                  non-d\'eterministes qui sont omnipr\'esents dans les
                  syst\`emes embarqu\'es.

                  Dans cet article, nous
                  pr\'esentons ProbZelus, une extension probabiliste
                  d'un langage synchrone descendant de Lustre.
                  ProbZelus permet de d\'ecrire des mod\`eles
                  probabilistes r\'eactifs, c'est-\`a-dire, en
                  interaction avec un environnement observable.  Lors
                  de l'ex\'ecution, un ensemble de techniques
                  d'inf\'erence peut \^etre utilis\'e pour apprendre les
                  distributions de param\`etres du mod\`ele \`a partir de
                  donn\'ees observ\'ees.  Nous illustrons l'expressivit\'e
                  de Probzelus avec des exemples comme un d\'etecteur
                  de trajectoire \`a partir d'observations bruit\'ees, ou
                  un contr\^oleur de robot capable d'inf\'erer \`a la fois
                  sa position et une carte de son environnement.},
  url = {jfla20.pdf}
}
@phdthesis{baudart:these17,
  author = {Guillaume Baudart},
  title = {{A Synchronous Approach to Quasi-Periodic Systems}},
  school = {\'Ecole normale sup\'erieure},
  year = 2017,
  address = {45 rue d'Ulm, 75230 Paris}
}
@inproceedings{lucy:fdl18,
  author = {Jean-Louis Colaco and Bruno Pagano
                  and C\'edric Pasteur and Marc Pouzet},
  title = {{Scade 6: from a Kahn Semantics to a Kahn Implementation for Multicore}},
  booktitle = {Forum on specification \& Design Languages (FDL)},
  year = 2018,
  month = {September},
  address = {Munich, Germany}
}
@inproceedings{lucy:pldi20,
  author = {Guillaume Baudart and Louis Mandel and
    Eric Atkinson and Benjamin Sherman and Marc Pouzet and Michael Carbin},
  title = {{Reactive Probabilistic Programming}},
  booktitle = {International Conference on Programming Language Design and
               Implementation (PLDI)},
  year = 2020,
  month = {June 15-20},
  address = {London, United Kingdom},
  organization = {ACM},
  abstract = {Synchronous modeling is at the heart of programming languages like
Lustre, Esterel, or Scade{} used routinely for implementing safety
critical control software, e.g., fly-by-wire and engine control in planes.
However, to date these languages have had limited modern support for
modeling uncertainty --- probabilistic aspects of the software's
environment or behavior --- even though modeling uncertainty is a
primary activity when designing a control system.

In this paper we present ProbZelus the first {\em synchronous
  probabilistic programming language}. 
ProbZelus conservatively provides the
facilities of a synchronous language to write control software, with
probabilistic constructs to model uncertainties and perform {\em
  inference-in-the-loop}.

We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to
separate deterministic and probabilistic expressions. We demonstrate a
semantics-preserving compilation into a first-order functional language
that lends itself to a simple presentation of inference algorithms for streaming models.
We also redesign the delayed sampling inference algorithm to provide efficient \emph{streaming} inference.
%for \ProbZelus models.
%
Together with an evaluation on several reactive applications, our results
demonstrate that ProbZelus enables the design of reactive probabilistic applications and efficient, bounded memory inference.
},
  url = {pldi2020-extended.pdf}
}
@inproceedings{lucy:arch-comp20,
  author = {Gidon Ernst and
                  Paolo Arcaini and
                  Ismail Bennani and
                  Alexandre Donz{\'e} and
                  Georgios Fainekos and
                  Goran Frehse and
                  Logan Mathesen and
                  Claudio Menghi and
                  Giulia Pedrielli and
                  Marc Pouzet and
                  Shakiba Yaghoubi and
                  Yoriyuki Yamagata and
                  Zhenya Zhang},
  title = {{ARCH-COMP} 2020 Category Report: Falsification},
  booktitle = {{ARCH20.} 7th International Workshop on Applied Verification of Continuous
                  and Hybrid Systems (ARCH20), Berlin, Germany, July 12, 2020},
  series = {EPiC Series in Computing},
  volume = {74},
  pages = {140--152},
  publisher = {EasyChair},
  year = {2020},
  url = {https://doi.org/10.29007/trr1},
  doi = {10.29007/trr1},
  timestamp = {Mon, 26 Jun 2023 20:48:58 +0200},
  biburl = {https://dblp.org/rec/conf/arch/ErnstABDFFMMPPY20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{lucy:arch-comp21,
  author = {Gidon Ernst and
                  Paolo Arcaini and
                  Ismail Bennani and
                  Aniruddh Chandratre and
                  Alexandre Donz{\'e} and
                  Georgios Fainekos and
                  Goran Frehse and
                  Khouloud Gaaloul and
                  Jun Inoue and
                  Tanmay Khandait and
                  Logan Mathesen and
                  Claudio Menghi and
                  Giulia Pedrielli and
                  Marc Pouzet and
                  Masaki Waga and
                  Shakiba Yaghoubi and
                  Yoriyuki Yamagata and
                  Zhenya Zhang},
  editor = {Goran Frehse and
                  Matthias Althoff},
  title = {{ARCH-COMP} 2021 Category Report: Falsification with Validation of
                  Results},
  booktitle = {8th International Workshop on Applied Verification of Continuous and
                  Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021},
  series = {EPiC Series in Computing},
  volume = {80},
  pages = {133--152},
  publisher = {EasyChair},
  year = {2021},
  url = {https://doi.org/10.29007/xwl1},
  doi = {10.29007/xwl1},
  timestamp = {Mon, 26 Jun 2023 20:48:58 +0200},
  biburl = {https://dblp.org/rec/conf/arch/ErnstABCDFFG0KM21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{lucy:emsoft21,
  author = {Timothy Bourke and
                  Paul Jeanmaire and
                  Basile Pesin and
                  Marc Pouzet},
  title = {Verified Lustre Normalization with Node Subsampling},
  journal = {{ACM} Trans. Embed. Comput. Syst.},
  volume = {20},
  number = {5s},
  pages = {98:1--98:25},
  year = {2021},
  note = {Paper presented at EMSOFT'21},
  abstract = {Dataflow languages allow the specification of reactive systems by mutually recursive stream equations, functions, and boolean activation conditions called clocks. Lustre and Scade are dataflow languages for programming embedded systems. Dataflow programs are compiled by a succession of passes.

This article focuses on the normalization pass which rewrites programs into the simpler form required for code generation.
V\'elus is a compiler from a normalized form of Lustre to CompCert's
Clight language. Its specification in the Coq interactive theorem prover includes an end-to-end correctness proof that the values prescribed by the dataflow semantics of source programs are produced by executions of generated assembly code. We describe how to extend V\'elus with a normalization pass and to allow subsampled node inputs and outputs. We propose semantic definitions for the unrestricted language, divide normalization into three steps to facilitate proofs, adapt the clock type system to handle richer node definitions, and extend the end-to-end correctness theorem to incorporate the new features. The proofs require reasoning about the relation between static clock annotations and the presence and absence of values in the dynamic semantics. The generalization of node inputs requires adding a compiler pass to ensure the initialization of variables passed in function calls.
},
  url = {emsoft21.pdf}
}
@inproceedings{lucy:jfla22,
  author = {Jean-Louis Colaco and Baptiste Pauget and Marc Pouzet},
  title = {{Inf\'erer et v\'erifier les tailles de tableaux avec
        des types polymorphes}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 2022,
  month = {28 juin-01 juillet},
  address = {Saint-M\'edard-d'Excideuil, Domaine d'Essendi\'eras (P\'erigord)},
  abstract = {Cet article pr\'esente un syst\`eme de v\'erification et d'inf\'erence        statique des tailles de tableaux dans un langage fonctionnel
        strict statiquement typ\'e.  Plut\^ot que de s'en remettre \`a des
        types d\'ependants, nous proposons un syst\`eme de types proche de
        celui de ML. Le polymorphisme sert \`a d\'efinir des fonctions
        g\'en\'eriques en type et en taille. L'inf\'erence permet une
        \'ecriture plus l\'eg\`ere des op\'erations classiques de traitement
        du signal --- application point-\`a-point, accumulation,
        projection, transpos\'ee, convolution --- et de leur
        composition~; c'est un atout clef de la solution propos\'ee. Pour
        obtenir un bon compromis entre expressivit\'e du langage des
        tailles et d\'ecidabilit\'e de la v\'erification et de l'inf\'erence,
        notre solution repose sur deux \'el\'ements~: (i) un langage de
        types o\`u les tailles sont des polyn\^omes multi-vari\'es et
        (ii)~l'insertion de points de coercition explicites entre
        tailles dans le programme source. Lorsque le programme est
        bien typ\'e, il s'ex\'ecute sans erreur de taille en dehors de ces
        points de coercition. Deux usages de la proposition faite ici peuvent \^etre envisag\'es~: (i) la g\'en\'eration de
        code d\'efensif aux points de coercition ou, (ii) pour les
        applications critiques ou intensives, la v\'erification statique
        des coercitions en les limitant \`a des expressions \'evaluables \`a
        la compilation ou par d'autres moyens de v\'erification formelle.
	
	
	L'article d\'efinit le langage d'entr\'ee, sa s\'emantique dynamique, son
	syst\`eme de types et montre sa correction. Il est accompagn\'e d'une
	impl\'ementation en \textsc{OCaml}, dont le code source est accessible
	publiquement.},
  url = {jfla22.pdf}
}
@inproceedings{lucy:jfla23,
  author = {Timothy Bourke and Basile Pesin and Marc Pouzet},
  title = {{Analyse de d\'ependance v\'erifi\'ee pour un langage synchrone \`a flot de donn\'ees}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 2023,
  month = {31 janvier -- 3 f\'evrier},
  address = {Praz-sur-Arly (Haute-Savoie)},
  abstract = {V\'elus est une formalisation d'un langage synchrone \`a flots de donn\'ees et de sa
compilation dans l'assistant de preuve Coq.
Il inclut une d\'efinition de la s\'emantique dynamique du langage,
un compilateur produisant du code imp\'eratif, et une preuve de bout en bout
que le compilateur pr\'eserve la s\'emantique des programmes.

Dans cet article, on sp\'ecifie dans V\'elus la s\'emantique de deux
structures d'activation pr\'esentes dans les compilateurs modernes:
switch et d\'eclarations locales.  Ces nouvelles constructions
n\'ecessitent une adaptation de l'analyse statique de d\'ependance de
V\'elus, qui produit un graphe acyclique comme t\'emoin de la bonne
formation d'un programme.  On utilise ce t\'emoin pour construire un
sch\'ema d'induction propre aux programmes bien form\'es.  Ce sch\'ema
permet de d\'emontrer le d\'eterminisme du mod\`ele s\'emantique dans Coq.  },
  url = {jfla23.pdf}
}
@inproceedings{lucy:array23,
  author = {Jean-Louis Colaco and
                  Baptiste Pauget and
		  Marc Pouzet},
  title = {{Polymorphic Types with Polymorphic Sizes}},
  booktitle = {Libraries, Languages and Compilers for Array Programming
  (ARRAY)},
  year = 2023,
  month = {18 June 2023},
  address = {Orlando, Florida, United States},
  organization = {ACM},
  abstract = {This article presents a compile-time analysis for tracking the size of data-structures in a statically typed and strict functional language. This information is valuable for static checking and code generation. Rather than relying on depen- dent types, we propose a type-system close to that of ML: polymorphism is used to define functions that are generic in types and sizes; both can be inferred. This approach is convenient, in particular for a language used to program critical embedded systems, where sizes are indeed known at compiletime. By using sizes that are multivariate polynomials, we obtain a good compromise between the expressiveness of the size language and its properties (verification, inference).
  
The article defines a minimal functional language that is sufficient to capture size constraints in types. It presents its dynamic semantics, the type system and inference algorithm. Last, we sketch some practical extensions that matter for a more realistic language.},
  url = {array23.pdf}
}
@inproceedings{lucy:ecrts23,
  author = {Timothy Bourke and Vincent Bregeon and Marc Pouzet},
  title = {Scheduling and Compiling Rate-Synchronous Programs with End-To-End Latency Constraints},
  booktitle = {Euromicro Conference on Real-Time Systesm (ECRTS)},
  year = 2023,
  pages = {1-22},
  month = {July},
  address = {Vienna},
  abstract = {We present an extension of the synchronous-reactive model for specifying multi-rate systems. A set of periodically executed components and their communication dependencies are expressed in a Lustre-like programming language with features for load balancing, resource limiting, and specifying end-to-end latencies. The language abstracts from execution time and phase offsets. This permits simple clock typing rules and a stream-based semantics, but requires each component to execute within an overall base period. A program is compiled to a single periodic task in two stages. First, Integer Linear Programming is used to determine phase offsets using standard encodings for dependencies and load balancing, and a novel encoding for end-to-end latency. Second, a code generation scheme is adapted to produce step functions. As a result, components are synchronous relative to their respective rates, but not necessarily simultaneous relative to the base period. This approach has been implemented in a prototype compiler and validated on an industrial application.},
  url = {ecrts23.pdf}
}
@inproceedings{lucy:emsoft23a,
  author = {Timothy Bourke and
                  Basile Pesin and
		  Marc Pouzet},
  title = {{Verified Compilation of Synchronous Dataflow with State Machines}},
  booktitle = {International Conference on Embedded Software (EMSOFT)},
  year = 2023,
  month = {September 17-22},
  address = {Hamburg, Germany},
  organization = {ACM},
  abstract = {Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the V\'elus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem.},
  url = {emsoft23a.pdf}
}
@inproceedings{lucy:emsoft23b,
  author = {Jean-Louis Colaco and
                  Michael Mendler and
		  Baptiste Pauget and
		  Marc Pouzet},
  title = {{A Constructive State-based Semantics and Interpreter for a Synchronous Data-flow Language with State machines}},
  booktitle = {International Conference on Embedded Software (EMSOFT)},
  year = 2023,
  month = {September 17-22},
  address = {Hamburg, Germany},
  organization = {ACM},
  abstract = {Scade is a domain-specific synchronous functional language used to implement safety-critical real-time software for more than twenty years. Two main approaches have been considered for its semantics: (i) an indirect collapsing semantics based on a source-to-source translation of high-level constructs into a data- flow core language whose semantics is precisely specified and is the entry for code generation; a relational synchronous semantics, akin to Esterel, that applies directly to the source. It defines what is a valid synchronous reaction but hides, on purpose, if a semantics exists, is unique and can be computed; hence, it is not executable.

This paper presents, for the first time, an executable, state-based semantics for a language that has the key constructs of Scade all together, in particular the arbitrary combination of data-flow equations and hierarchical state machines. It can apply directly to the source language before static checks and compilation steps. It is constructive in the sense that the language in which the semantics is defined is a statically typed functional language with call-by-value and strong normalization, e.g., it is expressible in a proof-assistant where all functions terminate. It leads to a reference, purely functional, interpreter. This semantics is modular and can account for possible errors, allowing to establish what property is ensured by each static verification performed by the compiler. It also clarifies how causality is treated in Scade compared with Esterel.

This semantics can serve as an oracle for compiler testing and validation; to prototype novel language constructs before they are implemented, to execute possibly unfinished models or that are correct but rejected by the compiler; to prove the correctness of compilation steps.

The semantics given in the paper is implemented as an interpreter in a purely functional style, in OCaml.},
  url = {emsoft23b-extended.pdf}
}
@unpublished{rml:simulation06,
  author = {Farid Benbadis and Louis Mandel and Marc Pouzet 
                  and Ludovic Samper},
  title = {{Simulation of Ad hoc Networks in ReactiveML}},
  note = {Submitted to journal publication},
  year = 2007,
  month = {Feb},
  url = {simulator-ad-hoc-networks06.pdf},
  abstract = {This paper presents a programming experiment of complex network
routing protocols for mobile ad hoc networks within the reactive
language ReactiveML.

Mobile ad hoc networks are highly dynamic networks characterized by
the absence of physical infrastructure. In such networks, nodes are
able to move, evolve concurrently and synchronize continuously with
their neighbors.  Due to mobility, connections in the network can
change dynamically and nodes can be added or removed at any time.  All
these characteristics~---~concurrency with many communications and the
need of complex data-structure~---~combined to our routing protocol
specifications make the use of standard simulation tools ({\it e.g.},
NS-2, OPNET) inadequate. Moreover network protocols appear to be very
hard to program efficiently in conventional programming languages.

In this paper, we show that the {\em synchronous reactive model} as
introduced in the pioneering work of Boussinot matters for programming
such systems. This model provides adequate programming constructs ---
namely synchronous parallel composition, broadcast communication and
dynamic creation --- which allow a natural implementation of the hard
part of the simulation. This thesis is supported by two concrete
examples: the first example is a routing protocol in mobile ad hoc
networks and the simulation focuses only on the network layer.  The
second one is a routing protocol for sensors networks and the wholes
layers are faithfully simulated (hardware, MAC and network
layers). More importantly, the physical environment (e.g., clouds) has
also been integrated into the simulation using the tool Lucky.

The implementation has been done in ReactiveML, an embedding of the reactive
model inside a statically typed, strict functional language. ReactiveML
provides reactive programming constructs together with most of the
features of Ocaml. Moreover, it provides an efficient execution
scheme for reactive constructs which made the simulation of real-size
examples (with several thousand of nodes) feasible.}
}
@inproceedings{rml:glonemo06,
  author = {Ludovic Samper and Florence Maraninchi and 
Laurent Mounier and Louis Mandel},
  title = {{GLONEMO}: Global and Accurate Formal Models for the 
Analysis of Ad-Hoc Sensor Networks},
  booktitle = {Proceedings of the First International 
Conference on Integrated Internet Ad hoc and Sensor Networks (InterSense'06)},
  year = {2006},
  address = {Nice, France},
  month = may
}
@inproceedings{rml:jfla14,
  author = {Louis Mandel and C{\'e}dric Pasteur},
  title = {Ex{\'e}cution efficace de programmes {ReactiveML}},
  url = {MandelPasteur-JFLA-2014.pdf}
}
@inproceedings{rml:sas14,
  author = {Louis Mandel and C{\'e}dric Pasteur},
  title = {Reactivity of Cooperative Systems},
  booktitle = {Proceedings of 21st International Static Analysis Symposium (SAS'14)},
  year = 2014,
  month = sep,
  address = {Munich, Germany},
  url = {MandelPasteur-SAS-2014.pdf},
  webpage = {http://reactiveml.org/sas14}
}
@inproceedings{rml:jfla05,
  author = {Louis Mandel et Marc Pouzet},
  title = {{{ReactiveML},
                  un langage pour la programmation r\'eactive en ML}},
  booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
  year = 2005,
  address = {Obernai, France},
  month = {Mars},
  publisher = {INRIA},
  url = {jfla05.ps.gz},
  abstract = {Nous pr\'esentons ReactiveML, un langage d\'edi\'e \`a la
programmation de syst\`emes r\'eactifs complexes tels que les
interfaces graphiques, les jeux vid\'eo ou les probl\`emes de
simulation.  Le langage est bas\'e sur le mod\`ele \emph{r\'eactif
synchrone} introduit dans les ann\'ees 90 par Fr\'ed\'eric Boussinot.
Ce mod\`ele combine les principes du mod\`ele synchrone avec la
possibilit\'e de cr\'eer dynamiquement des processus.

ReactiveML est une extension conservative d'un langage ML avec
appel par valeur. Il ajoute des constructions suppl\'ementaires
pour d\'ecrire les comportements temporels des syst\`emes.
Nous illustrons l'expressivit\'e du langage sur des exemples et
donnons une s\'emantique formelle du noyau du langage. La
s\'emantique exprime les interactions entre les expressions ML 
et les constructions r\'eactives. Le langage est statiquement 
typ\'e avec un syst\`eme d'inf\'erence de type \`a la Milner.
}
}
@inproceedings{rml:mandel-slap05,
  author = {Louis Mandel and Farid Benbadis},
  title = {{Simulation of Mobile Ad-Hoc Networks in {ReactiveML}}},
  booktitle = {{Synchronous Languages, Applications, and 
                  Programming (SLAP)}},
  editor = {Electronic Notes in Theoretical Computer Science},
  year = 2005,
  note = {available at \verb#www-spi.lip6.fr/~mandel/rml#},
  url = {mandel-slap05.ps.gz},
  abstract = {This paper presents a programming experiment of a complex
network routing protocol for mobile ad hoc networks within the ReactiveML
language.

Mobile ad hoc networks are highly dynamic networks characterized by
the absence of physical infrastructure. In such networks, nodes are
able to move, evolve concurrently and synchronize continuously with
their neighbors.  Due to mobility, connections in the network can
change dynamically and nodes can be added or removed at any time.  All
these characteristics~---~concurrency with many communications and the
need of complex data-structure~---~combined to our routing protocol
specifications make the use of standard simulation tools ({\it e.g.},
NS, OPNET) inadequate. Moreover network protocols appear to be very
hard to program efficiently in conventional programming languages.

In this paper, we show that the {\em synchronous reactive model}, as
introduced in the pioneering work of Boussinot, matters for
programming such systems. This model provides adequate programming
constructs --- namely synchronous parallel composition, broadcast
communication and dynamic creation --- which allow a natural
implementation of the hard part of the simulation.

The implementation has been done in ReactiveML, an embedding of the reactive
model inside a statically typed, strict functional language. ReactiveML 
provides reactive programming constructs together with most of the features
of Ocaml. Moreover, it provides an efficient execution scheme for
reactive constructs which made the simulation of real-size examples
feasible. Experimental results show that the ReactiveML implementation is
two orders of magnitude faster than the original C version; it was
able to simulate more than 1000 nodes where the original C version
failed (after 200 nodes) and compares favorably with the version programmed 
in NAB.}
}
@inproceedings{rml:ppdp05,
  author = {Louis Mandel and Marc Pouzet},
  title = {{ReactiveML, a Reactive Extension to ML}},
  booktitle = {ACM International Conference
                  on Principles and Practice of Declarative Programming
                  (PPDP)},
  year = 2005,
  address = {Lisboa},
  month = {July},
  url = {ppdp05.pdf},
  note = {Recipient of the price for the
          ``most influential PPDP'05  paper'' given in July 2015 at PPDP'15.},
  abstract = {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 {\em reactive} model introduced by Boussinot.  This model
combines the so-called {\em synchronous} model found in Esterel
which provides instantaneous communication and parallel composition
with classical features found in asynchronous models like dynamic
creation of processes.

The language comes as a conservative extension of an existing
call-by-value ML language and it provides additional constructs for
describing the temporal part of a system.
The language receives a behavioral
semantics {\em \`a la} Esterel and a transition semantics describing
precisely the interaction between ML values and reactive
constructs. It is statically typed through a Milner type inference
system and programs are compiled into regular ML programs.
The language has been used for programming several complex simulation
problems (e.g., routing protocols in mobile ad-hoc
networks).}
}
@phdthesis{rml:these-mandel06,
  author = {Louis Mandel},
  title = {Conception, S{\'e}mantique et Implantation de {ReactiveML} : un langage {\`a} la {ML} pour la programmation r{\'e}active},
  school = {Universit{\'e} Paris 6},
  year = {2006}
}
@article{rml:tsi08,
  author = {Louis Mandel and Marc Pouzet},
  title = {{ReactiveML} : un langage fonctionnel pour 
                  la programmation r{\'e}active},
  journal = {Techniques et Sciences Informatiques (TSI)},
  year = 2008,
  url = {tsi08.pdf}
}
@inproceedings{rml:mandel-plateau-slap08,
  author = {Louis Mandel and Florence Plateau},
  title = {Interactive Programming of Reactive Systems},
  booktitle = {Proceedings of Model-driven High-level Programming of Embedded Systems ({SLA++P'08})},
  year = 2008,
  month = apr,
  address = {Budapest, Hungary},
  url = {MandelPlateau-SLAP-2008.pdf}
}
@manual{rml:distribution,
  title = {The ReactiveML distribution},
  author = {Louis Mandel},
  organization = {Universit\'e Paris-Sud 11},
  note = {Available at: \texttt{rml.lri.fr}}
}
@inproceedings{rml:emsoft13,
  author = {Guillaume Baudart and Florent Jacquemard and
                  Louis Mandel and Marc Pouzet},
  title = {{A Synchronous Embedding of Antescofo, 
                   a Domain-Specific Language for Interactive Mixed Music}},
  booktitle = {International Conference on Embedded Software (EMSOFT)},
  year = 2013,
  editor = {ACM},
  month = {September 29-October 04},
  address = {Montreal},
  abstract = {Antescofo{} is a recently developed software for
                  \emph{musical score following} and \emph{mixed
                  music}: it automatically, and in real-time,
                  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 \emph{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.},
  url = {emsoft13.pdf}
}
@inproceedings{rml:farm13,
  author = {Guillaume Baudart and Louis Mandel and Marc Pouzet},
  title = {{Programming Mixed Music in ReactiveML}},
  booktitle = {Workshop on Functional Art, Music, Modeling and Design (FARM)},
  year = 2013,
  month = {September 28},
  address = {Boston},
  abstract = {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.},
  note = {Co-located with ICFP 2013},
  url = {farm13.pdf}
}
@inproceedings{rml:ppdp13,
  author = {Louis Mandel and C\'edric Pasteur and Marc Pouzet},
  title = {{Time Refinement in a Functional Synchronous Language}},
  booktitle = {15th International Symposium on Principles and Practice of Declarative Programming (PPDP)},
  year = 2013,
  month = {September 16-18},
  address = {Madrid, Spain},
  abstract = {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.},
  url = {ppdp13.pdf}
}
@article{rml:scp15,
  author = {Louis Mandel and C\'edric Pasteur and Marc Pouzet},
  title = {{Time Refinement in a Functional Synchronous Language}},
  journal = {Science of Computer Programming},
  year = 2015,
  note = {Available online 10 July 2015},
  abstract = {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.

                  The paper presents reactive
                  domains to simplify the programming of such
                  systems. Reactive domains allow for several time
                  scales to be defined and they enable time
                  refinement, that is, the replacement of a system
                  with a more detailed version, without changing its
                  observed behavior.

                  Our work applies to the
                  ReactiveML language, which extends an ML language
                  with synchronous programming constructs à la
                  Esterel. We present an operational semantics for the
                  extended language, a type system that ensures the
                  soundness of programs, and a sequential
                  implementation. We discuss how reactive domains can
                  be used in a parallel implementation.},
  url = {scp15.pdf}
}
@inproceedings{rml:ppdp15,
  author = {Louis Mandel and C\'edric Pasteur and Marc Pouzet},
  title = {{ReactiveML, Ten Years Later}},
  booktitle = {ACM International Conference
                  on Principles and Practice of Declarative Programming
                  (PPDP)},
  year = 2015,
  address = {Siena, Italy},
  month = {July},
  url = {ppdp15.pdf},
  note = {Invited paper for PPDP'05 award.},
  abstract = {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 real-time
                  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.

While all ReactiveML programs presented at PPDP'05
                  still compile, the language has evolved continuously
                  to incorporate novel programming constructs,
                  compilation techniques and dedicated static
                  analyses. ReactiveML has been used for applications
                  that we never anticipated: the simulation of
                  large-scale ad-hoc and sensor networks, an
                  interactive debugger, and interactive mixed
                  music. These applications were only possible due to
                  the efficient compilation of ReactiveML into
                  sequential code, which we present here for the first
                  time. We also present a parallel implementation that
                  uses work-stealing techniques through shared
                  memory. Finally, we give a retrospective view on
                  ReactiveML over the past ten years.}
}
@phdthesis{rml:these-pasteur13,
  author = {C\'edric Pasteur},
  title = {{Raffinement temporel et ex\'ecution parall\`ele dans un langage synchrone fonctionnel}},
  school = {Universit\'e Pierre et Marie Curie},
  year = 2013,
  address = {Paris, France},
  month = {26 novembre},
  url = {http://www.di.ens.fr/~pasteur/}
}

This file was generated by bibtex2html 1.99.