Fakultätskolloquium "A Functional Language with Time Warps" (Dr. Adrien Guatto, INRIA, Paris)

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 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.