Towards a common categorical semantics for linear-time temporal logic and functional reactive programming

W Jeltsch - Electronic Notes in Theoretical Computer Science, 2012 - Elsevier
W Jeltsch
Electronic Notes in Theoretical Computer Science, 2012Elsevier
Linear-time temporal logic (LTL) and functional reactive programming (FRP) are related via
a Curry–Howard correspondence. Based on this observation, we develop a common
categorical semantics for a subset of LTL and its corresponding flavor of FRP. We devise a
class of categorical models, called fan categories, that explicitly reflect the notion of time-
dependent trueness of temporal propositions and a corresponding notion of time-dependent
type inhabitance in FRP. Afterwards, we define the more abstract concept of temporal …
Linear-time temporal logic (LTL) and functional reactive programming (FRP) are related via a Curry–Howard correspondence. Based on this observation, we develop a common categorical semantics for a subset of LTL and its corresponding flavor of FRP. We devise a class of categorical models, called fan categories, that explicitly reflect the notion of time-dependent trueness of temporal propositions and a corresponding notion of time-dependent type inhabitance in FRP. Afterwards, we define the more abstract concept of temporal category by extending categorical models of intuitionistic S4. We show that fan categories are a special form of temporal categories.
Elsevier