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

  • April 25, 2014 · 6:30 PM
  • This location is shown only to members

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.

Join or login to comment.

  • Lance

    so sad i missed this, sounds like an awesome topic. would you think about having this again?!?

    October 29

    • Sergei W.

      Not sure about repeating, but take a look at the talk slides!

      October 30

  • Sergei W.

    For an introduction to Curry-Howard isomorphism, perhaps Wadler's "Proofs are programs" is the best reading. http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf

    April 27, 2014

    • steck

      Umm, I just mentioned that one on this board. ;-)

      April 27, 2014

    • Sergei W.

      Yes, you did! I just meant to say that Wadler's paper is perhaps best to be read as a first exposition.

      April 27, 2014

  • Sergei W.

    Here is a paper that introduces some important technical concepts in logic: axioms, natural deduction systems, sequents, and how they are related to the Curry-Howard isomorphism. I am reading this now, hoping to clarify these things a bit more for myself. Ariola, Bohannon, Sabri. Sequent calculi and abstract machines. http://www.cs.indiana.edu/~sabry/papers/sequent.pdf

    April 27, 2014

  • Valeria De P.

    Really a great talk, Sergei. I learned a lot about why do we want this kind of temporal logic and also about transforming it into automata theory, thanks!

    April 26, 2014

    • Sergei W.

      Thank you! If you took interest to the LTL -> Automata translation, I should warn you that I have glossed over many, many details. I wanted to show only the bare minimum necessary to understand why this kind of translation makes sense.

      1 · April 26, 2014

  • Valeria De P.

    Sergei forgot to add to his suggested reading `On the Unusual Effectiveness of Logic in Computer Science' that he discussed at the beginning of his talk, the link is http://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf. People might also enjoy the predecessors of this paper, linked from my blog post http://logic-forall.blogspot.com/2011/04/problems-and-materials.html

    April 26, 2014

  • steck

    Someone asked about Curry-Howard. Here's a paper by Wadler that introduces it: http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf

    1 · April 25, 2014

  • Sergei W.

    To answer Valeria's question about whether the strict Until or the weak Until is useful in programming, I would say that having at least one of them seems to be useful, but I do not see the practical necessity of having both of them in the same programming language.

    April 25, 2014

  • Sergei W.

    For people who could not attend (including the guys on the 8:35 train, care to introduce yourself?) - here are my slides (with the ab'c' mistake corrected).
    https://drive.google.com/file/d/0B3EMdMSL-DnmYWEyMFM3d0NMX2M/

    1 · April 25, 2014

  • Michael F.

    Sergei's talk was great, and so were the slides. He has obviously researched the topic thoroughly, and has arrived at some simple, clearly presented conclusions.

    1 · April 25, 2014

  • Ian Z.

    Mmm, I would love to but this is a bit too far for me. Will any artefacts (notes, even slides :-p ) be available?

    April 16, 2014

    • Sergei W.

      I will have slides posted.

      April 17, 2014

  • Sergei W.

    People not familiar with mu-calculus, please don't worry: I found a way to explain what it is rather quickly and easily.

    2 · April 3, 2014

  • Sergei W.

    Krishnaswamy's paper is the only one that uses full temporal mu-calculus as the type system for FRP. (Other people use only fragments of temporal logic.)

    April 3, 2014

  • Sergei W.

    One more important (imho) paper,

    N. R. Krishnaswami. Higher-order functional reactive programming without spacetime leaks (2013). https://www.mpi-sws.org/~neelk/simple-frp.pdf

    I will definitely talk about some stuff from this paper. It presents a model of FRP that is much closer to what I would consider to be ideal. Also, the author has implemented his FRP in a toy language "AjdS" available here, http://www.mpi-sws.org/~neelk/

    1 · April 3, 2014

  • Valeria De P.

    Yay, Sergei! Sounds fantastic. great biblio, how old is the thesis? around 2000? Alan Jeffrey has a new paper that he announced in facebook http://ect.bell-labs.com/who/ajeffrey/papers/lics14.pdf

    April 2, 2014

    • Sergei W.

      Interesting paper, I'll have a look! Thanks!

      1 · April 2, 2014

  • Christopher B.

    Another FYI re linear types -- SF Computer Language Design and Implementation has an upcoming meetup April 8 on "Mozilla's Rust language and possibly something on linear types or inferring ownership transfer type stuff. " http://www.meetup.com/SF-Computer-Language-Design-and-Implementation/events/170212732/

    1 · April 2, 2014

Imagine having a community behind you

Get started Learn more
Rafaël

We just grab a coffee and speak French. Some people have been coming every week for months... it creates a kind of warmth to the group.

Rafaël, started French Conversation Group

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy