Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Lundi 2 février, 10h30 ------------- Adrien Guatto ------------- ENS ===================================================== A Functional Synchronous Language with Integer Clocks ===================================================== Synchronous languages in the vein of Lustre are first-order functional languages dedicated to stream processing. Lustre compilers use a type-like static analysis, the _clock calculus_, to reject programs that cannot be implemented as finite state machines. The broad idea is to assign to each element of a stream a logical computation date in a global, discrete time scale. When this analysis succeeds, the types obtained guide the code generation phase of the compiler, which produces transition functions. In practice, these functions consists in simple, bounded memory C code featuring only assignments and conditional statements. This talk presents a variation on Lustre and its compilation. Our proposal is twofold. First, we add a new construct that creates a local time scale whose internal steps are invisible from the outside. Second, we change the clock calculus to allow several elements of a stream to be computed during the same time step. I will discuss the resulting type system and its soundness proof, which relies on an elementary form of step-indexed realizability. If time permits, I will also describe how the code generation scheme of Lustre, once adapted to this new setting, generates code featuring nested loops.