2019/03/14 by Patrick Bahr, Bahr, Patrick, Christian Uldal Graulund +3 · 2 citations
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1903.05879
openalex publication_date 2019/03/14 · openalex created_date 2022/07/29 · openalex updated_date 2026/07/28
Functional reactive programming (FRP) is a paradigm for programming with\nsignals and events, allowing the user to describe reactive programs on a high\nlevel of abstraction. For this to make sense, an FRP language must ensure that\nall programs are causal, and can be implemented without introducing space leaks\nand time leaks. To this end, some FRP languages do not give direct access to\nsignals, but just to signal functions.\n Recently, modal types have been suggested as an alternative approach to\nensuring causality in FRP languages in the synchronous case, giving direct\naccess to the signal and event abstractions. This paper presents Simply RaTT, a\nnew modal calculus for reactive programming. Unlike prior calculi, Simply RaTT\nuses a Fitch-style approach to modal types, which simplifies the type system\nand makes programs more concise. Echoing a previous result by Krishnaswami for\na different language, we devise an operational semantics that safely executes\nSimply RaTT programs without space leaks.\n We also identify a source of time leaks present in other modal FRP languages:\nThe unfolding of fixed points in delayed computations. These time leaks are\neliminated by the Simply RaTT type system.\n