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 - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 6 novembre, 10h30

                                -------------
                                Adrien Guatto
                                -------------

                                 Inria Paris

                    =====================================
                    A Functional Language with Time Warps
                    =====================================

Synchronous dataflow languages in the vein of Lustre combine a high-level
programming model with strong safety guarantees enforced at compile time. They
are built on the idea of logical time: programs manipulate infinite streams of
data which unfold progressively as time passes. Whether a stream unfolds at any
given time step is determined by a type-like formula, its clock. Clocks are an
essential ingredient of synchronous compilation; for instance, they are used to
to bound memory usage and rule out deadlocks in recursive stream definitions.

Proof assistants based on type theory, like Coq, also provide infinite streams
and face some of the same challenges as synchronous languages. In particular, to
preserve logical soundness they must ensure that any finite prefix of a stream
can be computed in finite time. Recent work on so-called guarded type theories
solve this problem through the introduction of a new type former, the later
modality, expressing that a piece of data will only be available at the next
time step. The fact that this modality can be applied to any type makes it more
general than synchronous clocks, which only deal with streams. For instance, it
allows recursive function definitions.

In this talk, I will present Pulsar, a simply-typed lambda-calculus with
infinite streams inspired from synchronous languages and guarded type
theories. Pulsar features a new modality indexed by deformations of the logical
time scale that we call warps. Warps generalize both the later modality and
synchronous clocks, allowing the language to capture recursive stream and
function definitions hitherto out of reach of existing systems. I will introduce
Pulsar through examples, present its type system, discuss its semantics, and
sketch a type-checking algorithm.