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.

About these ads

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

  1. asajeffrey says:

    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.

  2. […] recently gave a talk about the main points of my MFPS ’12 paper. The title of the talk was Categorical Models for Two Intuitionistic Modal […]

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