New paper about a generalization of FRP and causality in categorical models

Yesterday I finished my new paper Temporal Logic with “Until”, Functional Reactive Programming with Processes, and Concrete Process Categories, which will appear in the proceedings of PLPV ’13 and is also available online. I have already given two talks on topics of this paper, one at the Joint Estonian–Latvian Theory Days at Medzābaki and another one at the Theory Seminar of the Institute of Cybernetics.

The paper covers two topics:

An FRP analog of “until” proofs
Temporal logic and FRP are connected via a Curry–Howard correspondence. Thereby the “always” modality corresponds to the type constructor for behaviors, and the “eventually” modality corresponds to the type constructor for events. However there are more temporal operators. One example is the “until” operator from LTL. The paper shows that a proof of an “until” proposition can be regarded as an FRP value that consists of a finite time-varying value and a terminal event. I call such a value a process. It has turned out that processes are a really useful concept for reactive programming, in particular, when they are combined with recursion. The paper gives several examples of their use.
Causality in categorical models of FRP
In Section 2 of my MFPS paper, I presented a rather simple categorical semantics for temporal logic and FRP, which directly expresses time-dependence of trueness in temporal logic and of type inhabitance in FRP. However this semantics also models noncausal FRP operations, which actually cannot occur in real life. The new paper presents an improved version of the simple categorical semantics that takes causality into account. Its key idea is to deal with the time-dependent knowledge about values instead of the values themselves.

Happy reading!

When replying to another comment, please press that comment’s “Reply” button first.

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s