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.


4 thoughts on “New paper about categorical models of temporal logic and FRP

  1. asajeffrey

    Glad 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.

    1. Wolfgang Jeltsch Post author

      I 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.

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

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

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

You are commenting using your 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