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!
