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.

### Like this:

Like Loading...

asajeffreyGlad to see a writeup of this! Pity I’m not going to be at MFPS. I don’t think I’ve been a tag before.

Wolfgang JeltschPost authorI hope it’s no problem for you to be a tag. 🙂 It’s a general policy of mine to also have the names of persons mentioned in articles as tags, so that you can look for all articles that are related to a certain person.

asajeffreyI’m quite happy to be a tag. If you want to link to my (somewhat sporadic) G+ page, I’m https://plus.google.com/111927747393309805563

Pingback: Talk about categorical models of temporal logic and FRP « Wolfgang Jeltsch