New paper about categorical models of temporal logic and FRP

Temporal logic and functional reactive programming are related via a Curry–Howard correspondence, as has recently be shown by Alan Jeffrey and by myself. Given this intriguing connection, it seems to be worthwhile to look for a common categorical semantics of temporal logic and FRP. This undertaking is a current research topic of mine. I will present some results on this at this year’s MFPS conference under the title Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. A preprint of the corresponding paper is now available online.

The logic I consider in this paper is a subset of an intuitionistic LTL whose only modalities are future-only variants of the “globally” and “finally” operators. I build categorical models of this logic by extending categorical models of intuitionistic S4 variants as follows:

• Instead of the comonads and monads that are used for modeling □ and ◇ in intuitionistic S4 models, I use ideal comonads and ideal monads. This accommodates the fact that the “globally” and “finally” modalities refer only to the future, not to the present.
• I require the existence of certain products in the Kleisli categories of the abovementioned monads. The existence of these products corresponds to the fact that times are totally ordered.

I will give a talk on this topic on May 10 and provide a link to its slides once they are ready.