Seminar details
Abstract: 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 bound memory usage and rule out deadlocks.
Some 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 observed 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. This modality may appear to be a special case of synchronous clocks at first, but is in fact more general in the sense that it applies to arbitrary types, rather than just streams.
In this talk, I will present Pulsar, a 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 can express the later modality as well as synchronous clocks, but also many new possibilities. Using warps, Pulsar's types can capture fine-grained dependencies between computations, and thus accept recursive stream definitions out of reach of existing languages. I will introduce the language through examples, present its type system, and discuss its semantics.
