English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

When designing languages for functional reactive programming (FRP) the mainchallenge is to provide the user with a simple, flexible interface for writingprograms on a high level of abstraction while ensuring that all programs can beimplemented efficiently in a low-level language. To meet this challenge, a newfamily of modal FRP languages has been proposed, in which variants of Nakano'sguarded fixed point operator are used for writing recursive programsguaranteeing properties such as causality and productivity. As an apparentextension 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 intypes. However, these two ideas are in conflict with each other, since thefixed point operator introduces non-termination into the inductive types thatare supposed to provide termination guarantees.  In this paper we show that by regarding the modal time step operator of LTL asubmodality of the one used for guarded recursion (rather than equating them),one can obtain a modal type system capable of expressing liveness propertieswhile retaining the power of the guarded fixed point operator. We introduce thelanguage Lively RaTT, a modal FRP language with a guarded fixed point operatorand an `until' type constructor as in LTL, and show how to program with eventsand fair streams. Using a step-indexed Kripke logical relation we proveoperational properties of Lively RaTT including productivity and causality aswell as the termination and liveness properties expected of types from LTL.Finally, we prove that the type system of Lively RaTT guarantees the absence ofimplicit space leaks.

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