Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 18:30 - 18:40 at POPL-B - Types and Functional Languages

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 of abstraction while ensuring that all programs can be implemented efficiently in a low-level language. To meet this challenge, a new family of modal FRP languages has been proposed, in which variants of Nakano’s guarded fixed point operator are used for writing recursive programs guaranteeing properties such as causality and productivity. As an apparent extension to this it has also been suggested to use Linear Temporal Logic (LTL) as a language for reactive programming through the Curry-Howard isomorphism, allowing properties such as termination, liveness and fairness to be encoded in types. However, these two ideas are in conflict with each other, since the fixed point operator introduces non-termination into the inductive types that are supposed to provide termination guarantees.

In this paper we show that by regarding the modal time step operator of LTL a submodality of the one used for guarded recursion (rather than equating them), one can obtain a modal type system capable of expressing liveness properties while retaining the power of the guarded fixed point operator. We introduce the language Lively RaTT, a modal FRP language with a guarded fixed point operator and an ‘until’ type constructor as in LTL, and show how to program with events and fair streams. Using a step-indexed Kripke logical relation we prove operational properties of Lively RaTT including productivity and causality as well as the termination and liveness properties expected of types from LTL. Finally, we prove that the type system of Lively RaTT guarantees the absence of implicit space leaks.

Thu 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30: Types and Functional LanguagesPOPL at POPL-B
18:30 - 18:40
Talk
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
POPL
Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen
Link to publication DOI
18:40 - 18:50
Talk
On the Semantic Expressiveness of Recursive Types
POPL
Marco PatrignaniStanford University, USA / CISPA, Germany, Eric Mark MartinStanford, Dominique DevrieseVrije Universiteit Brussel
Link to publication DOI
18:50 - 19:00
Talk
Automatic Differentiation in PCF
POPL
Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris
Link to publication DOI Pre-print
19:00 - 19:10
Talk
Intersection Types and (Positive) Almost-Sure Termination
POPL
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Claudia FaggianUniversité de Paris & CNRS, Simona Ronchi Della RoccaUniversity of Torino
Link to publication DOI
19:10 - 19:20
Talk
Intensional Datatype Refinement
POPL
Eddie JonesUniversity of Bristol, Steven RamsayUniversity of Bristol
Link to publication DOI
19:20 - 19:30
Talk
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Felipe Bañados SchwerterUniversity of British Columbia, Alison M. ClarkUniversity of British Columbia, Khurram A. JaferyUniversity of British Columbia, Ronald GarciaUniversity of British Columbia
Link to publication DOI