ITU

Diamonds are not forever: Liveness in reactive programming with guarded recursion

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Standard

Diamonds are not forever: Liveness in reactive programming with guarded recursion. / Bahr, Patrick; Graulund, Christian Uldal; Møgelberg, Rasmus Ejlers.

ACM SIGPLAN Symposium on Principles of Programming Languages. Vol. 5 POPL. ed. Association for Computing Machinery, 2021. (Proceedings of the ACM on Programming Languages).

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Harvard

Bahr, P, Graulund, CU & Møgelberg, RE 2021, Diamonds are not forever: Liveness in reactive programming with guarded recursion. in ACM SIGPLAN Symposium on Principles of Programming Languages. POPL edn, vol. 5, Association for Computing Machinery, Proceedings of the ACM on Programming Languages. https://doi.org/10.1145/3434283

APA

Bahr, P., Graulund, C. U., & Møgelberg, R. E. (2021). Diamonds are not forever: Liveness in reactive programming with guarded recursion. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ed., Vol. 5). Association for Computing Machinery. Proceedings of the ACM on Programming Languages https://doi.org/10.1145/3434283

Vancouver

Bahr P, Graulund CU, Møgelberg RE. Diamonds are not forever: Liveness in reactive programming with guarded recursion. In ACM SIGPLAN Symposium on Principles of Programming Languages. POPL ed. Vol. 5. Association for Computing Machinery. 2021. (Proceedings of the ACM on Programming Languages). https://doi.org/10.1145/3434283

Author

Bahr, Patrick ; Graulund, Christian Uldal ; Møgelberg, Rasmus Ejlers. / Diamonds are not forever: Liveness in reactive programming with guarded recursion. ACM SIGPLAN Symposium on Principles of Programming Languages. Vol. 5 POPL. ed. Association for Computing Machinery, 2021. (Proceedings of the ACM on Programming Languages).

Bibtex

@inproceedings{f57dac1e243741b9b7a72f50ead52087,
title = "Diamonds are not forever: Liveness in reactive programming with guarded recursion",
abstract = "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.",
author = "Patrick Bahr and Graulund, {Christian Uldal} and M{\o}gelberg, {Rasmus Ejlers}",
year = "2021",
month = jan,
doi = "https://doi.org/10.1145/3434283",
language = "English",
volume = "5",
series = "Proceedings of the ACM on Programming Languages",
publisher = "Association for Computing Machinery",
booktitle = "ACM SIGPLAN Symposium on Principles of Programming Languages",
address = "United States",
edition = "POPL",

}

RIS

TY - GEN

T1 - Diamonds are not forever: Liveness in reactive programming with guarded recursion

AU - Bahr, Patrick

AU - Graulund, Christian Uldal

AU - Møgelberg, Rasmus Ejlers

PY - 2021/1

Y1 - 2021/1

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

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

U2 - https://doi.org/10.1145/3434283

DO - https://doi.org/10.1145/3434283

M3 - Article in proceedings

VL - 5

T3 - Proceedings of the ACM on Programming Languages

BT - ACM SIGPLAN Symposium on Principles of Programming Languages

PB - Association for Computing Machinery

ER -

ID: 85724925