Thursday, April 21, 2016

The Essence of Event-Driven Programming

Together with Jennifer Paykin and Steve Zdancewic, I have a new draft paper, The Essence of Event-Driven Programming:

Event-driven programming is based on a natural abstraction: an event is a computation that can eventually return a value. This paper exploits the intuition relating events and time by drawing a Curry-Howard correspondence between a functional event-driven programming language and a linear-time temporal logic. In this logic, the eventually proposition ◇A describes the type of events, and Girard’s linear logic describes the effectful and concurrent nature of the programs. The correspondence reveals many interesting insights into the nature of event- driven programming, including a generalization of selective choice for synchronizing events, and an implementation in terms of callbacks where ◇A is just ¬□¬A.

If you've been following the work on temporal logic and functional reactive programming that I and others (e.g., Alan Jeffrey, Wolfgang Jeltsch, Andrew Cave et al) have been pursuing for a while, then you'll have heard that there's a really compelling view of reactive programs as proof terms for linear temporal logic.

However, the programs that come out seem to be most naturally conceived of as a kind of "higher-order synchronous dataflow" (in the same space as languages like ReactiveML or Lucid). These languages are based on the synchrony hypothesis, which postulates that programs do relatively little work relative to the clock rate of the event loop, and so a polling implementation where programs wake up once on each trip through the event loop is reasonable. (If you've done game programming, you may be familar with the term immediate mode GUI, which is basically the same idea.

But most GUI toolkits typically are not implemented in this style. Instead, they work via callbacks, in an event-driven style. That is, you write little bits of code that get invoked for you whenever an event occurs. The advantage of this is that it lets your program sleep until an event actually happens, and when an event happens, only the relevant pieces of your program will run. For applications (like a text editor) where the display doesn't change often and events happen at a relatively low clock rate, you can avoid a lot of useless computation.

In this paper, we show that the event-based style also fits into the temporal logic framework! Basically, we can encode events (aka promises or futures) using the double-negation encoding of the possibility monad from modal logic. And then the axioms of temporal logic (such as the linearity of time) work out to be natural primitives of event-based programming, such as the select operator.

Also, before you ask: an implementation is in progress, but not yet done. I'll post a link when it works!

Tuesday, April 19, 2016

Postdoctoral Position in Recursion, Guarded Recursion and Computational Effects

We are looking for a Postdoctoral Research Fellow to work on an EPSRC-funded project Recursion, Guarded Recursion and Computational Effects.

We shall be investigating fine-grained typed calculi and operational, denotational and categorical semantics for languages that combine either guarded or general recursion and type recursion with a range of computational effects. This will build on existing work such as call-by-push-value and Nakano's guarded recursion calculus.

The successful candidate will have a PhD in programming language semantics or a related discipline, and an ability to conduct collaborative mathematical research. Knowledge of operational and denotational semantics, category theory, type theory and related subjects are all desirable.

You will work with Paul Levy (principal investigator) and Neelakantan Krishnaswami (co-investigator) as part of the Theoretical Computer Science group at the University of Birmingham.

The position lasts from 1 October 2016 until 30 September 2019.

You can read more and apply for the job at:

Don't hesitate to contact us (particularly Paul Levy) informally to discuss this position.

The closing date is soon: 22 May 2016.

Reference: 54824 Grade point 7 Starting salary £28,982 a year, in a range up to £37,768 a year.