Temporal Logic and Functional Reactive Programming (talk by Sergei Winitzki)

Abstract: In my day job, most bugs come from imperatively implemented reactive programs. Temporal Logic and FRP are declarative approaches that promise to solve my problems. I will briefly review the motivations behind and the connections between temporal logic and FRP. I propose a rather "pedestrian" approach to propositional linear-time temporal logic (LTL), showing how to perform calculations in LTL and how to synthesize programs from LTL formulas. Hopefully, I will have time to explain why LTL largely failed to solve the synthesis problem, and how FRP tries to cope.

Literature: It is optional to read anything in this list. My talk will be largely self-contained and should be understandable to anyone familiar with Curry-Howard and functional programming.

E. Czaplicki, S. Chong. Asynchronous FRP for GUIs. (2013) http://people.seas.harvard.edu/~chong/pubs/pldi13-elm.pdf
Explains the type system of ELM, an FRP language implemented by the author. This is a clean and simple presentation of a small language and type system. Neither too abstract for my taste, nor too low-level. I would start by reading this.

E. Czaplicki. Concurrent FRP for functional GUI (2012). http://www.seas.harvard.edu/sites/default/files/files/archived/Czaplicki.pdf
Looks like MS thesis of the same author; slightly more discussion and detail on ELM. Optional.

Lecture slides: A Hilbert-style proof system for LTL http://www.csc.kth.se/~mfd/...logic/lecture2.pdf
Read this only if you are already quite familiar with logic and proof systems. I will only use the list of axioms to illustrate the choice of FRP primitives via Curry-Howard.

E. Bainomugisha, et al. A survey of reactive programming. 2013.
ftp://progftp.vub.ac.be/tech_report/2012/vub-soft-tr-12-13.pdf
A survey of existing FRP implementations. No theory, very hands-on approach, as might be guessed by looking at the first author's first name ("Engineer").

W. Jeltsch. Temporal logic with Until, Functional Reactive Programming with processes, and concrete process categories. http://www.ioc.ee/~wolfgang/research/plpv-2013-paper.pdf
A. Jeffrey. LTL types FRP. http://ect.bell-labs.com/who/ajeffrey/papers/plpv12.pdf
These two papers explain the Curry-Howard correspondence between (intuitionistic, linear-time) temporal logic and FRP. The papers are somewhat abstract.

D. Marchignoli. Natural deduction systems for temporal logic. http://phd.di.unipi.it/Theses/PhDthesis_Marchignoli.pdf
This is a doctoral thesis; Chapter 2 contains many basic definitions, in particular, it presents a natural deduction system for modal and temporal logics. I am not going to discuss this very much; I put in this reference for people who might be more inclined to study temporal logic as a formal system.