5 papers
Diamonds are not forever: Liveness in reactive programming with guarded recursion
Patrick Bahr, Christian Uldal Graulund, Rasmus Møgelberg
When designing languages for functional reactive programming (FRP) the main challenge is to provide the user with a simple, flexible interface for writing programs on a high level…
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming without Space Leaks
Patrick Bahr, Christian Graulund, Rasmus Møgelberg
Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For thi…
Bisimulation as path type for guarded recursive types
Rasmus Ejlers Møgelberg, Niccolò Veltri
In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based o…
The clocks they are adjunctions:Denotational semantics for Clocked Type Theory
Bassel Mannaa, Rasmus Ejlers Møgelberg
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning ab…
Denotational semantics for guarded dependent type theory
Aleš Bizjak, Rasmus Ejlers Møgelberg
We present a new model of Guarded Dependent Type Theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with, and reason about coinductive…