Name: Temporal Logic and Functional Reactive Programming (talk by Sergei Winitzki)
Start: 2014-04-25T18:30:00-07:00
End: 2014-04-25T21:30:00-07:00
Location: Room EC326, Bannan Engineering Building, Santa Clara University

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.

Vlad Patryshev

Bay Area Categories And Types

Technology

Logic

Category Theory

Functional Programming

Type Theory

Functors and Monads

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

Room EC326, Bannan Engineering Building, Santa Clara University

Share

Bay Area Categories And Types

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

Bay Area Categories And Types

Details

Members are also interested in