Institute of Cybernetics at TUT
Thursday, 4 October 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Functional reactive programming (FRP) is a declarative programming paradigm that uses so-called behaviors and events for describing temporal behavior. FRP is related to an intuitionistic temporal logic via a Curry-Howard correspondence. Thereby the type constructors for behaviors and events correspond to the always and eventually modalities. In this talk, we show that the until operators from linear-time temporal logic (LTL) give rise to an FRP notion called processes, which generalizes behaviors and events. Afterwards we present a categorical semantics for FRP with processes and intuitionistic temporal logic with until. This semantics expresses causality of FRP operations using standard constructs from category theory. It achieves this by focusing on the time-dependent knowledge about values, not on the values themselves. We show that this approach makes it impossible to express liveness conditions under certain conditions.