When it rains, it pours

Having written a new paper on FRP of my own, I've just discovered that lots of other people have been hard at work in this area.

• Alan Jeffrey has a new paper for PLPV 2013, entitled Causality For Free!: Parametricity Implies Causality for Functional Reactive Programs.

  This looks very interesting, since it looks like he's found a different way of enforcing causality than the one Nick and I hit on. We formalized the order structure of time (this happens before that), and required functions to respect that order. Alan has a discrete model of time (i.e., he doesn't bake temporal order into his category of times), and instead he uses parametricity to prove that all the definable functions (of the appropriate type) are inherently causal.

• Wolfgang Jeltsch also has a new paper for PLPV 2013, entitled Temporal Logic with “Until”, Functional Reactive Programming with Processes, and Concrete Process Categories.

  He's also been looking at using full temporal logic for typing reactive programs. This paper looks especially focused on the distinction between strong (must eventually happen) and weak eventually (may eventually happen) operators.

• Brigitte Pientka visited us here at MPI last week, and she told me about some work that some of her students (Francisco Ferreira and someone whose name I unfortunately cannot recall -- Andrew Cave?) have been doing with her and Prakash Panangaden, on giving a proof theory for the modal mu-calculus. At a high level, their calculus looks very similar to the system I just wrote up, but there are some very intriguing semantic differences.

  I use a Nakano-style guarded recursive type, which allows negative occurences. This permits defining general fixed points $(\bullet{A} \to A) \to A$, which collapses greatest and least fixed points. They use strict positivity instead, and so they can distinguish them, at the cost of more restrictive typing of recursive definitions. (This ties into Jeltsch's work on strong/weak eventually, which correspond to inductive versus coinductive definitions of the eventually type.)

  Limit-colimit coincidence is one of the most striking features of categories of pointed domains, and it's (a) interesting that it can be induced already with guarded recursion, and (b) it might be easier to study in this setting.

• Marc Bagnol and Adrien Guatto have written a draft paper, Synchronous Machines: a Traced Category.

  The basic idea, roughly speaking, is to start with Mealy automata as a model of reactive programs. These automata lack a notion of higher-order behavior, but if you hit them with the Geometry of Interaction construction, you can get out a higher-order (linearly-typed) programming language, which is still implementable with finite state. This is a very nice idea, and reminiscent of Dan Ghica's work on synthesizing circuits.