PLPV

This is the first of a series of posts based on experiences at POPL (Principles of Programming Languages), 2012, in Philadelphia PA.

PLPV (Programming Languages meet Program Verification) is a workshop co-located with POPL, that focuses on ways to reduce the burden of program verification by exploiting properties of the underlying programming language (e.g., types, contracts).

Alan Jeffrey (Bell Labs) gave the first talk of the morning, digging into an intriguing connection between linear temporal logic (LTL) and functional reactive programming (FRP) via the Curry-Howard isomorphism. The basic idea is that because signals in FRP are time-indexed values, their types should be time-indexed as well: but time-indexed types can be read as LTL formulas, following the “types as propositions” slogan. One interesting observation was that the “until” modality in LTL does not have a natural programming interpretation, but its dual, the “constrains” modality, does. (Recall that, for any formulae A, B: A “constrains” B holds at time S whenever, for all times T >= S, if A holds in the interval [S,T) then B holds at T.) In particular, whereas the “constrains” modality forms the basis of compositional reasoning about rely/guarantee properties of concurrent systems, it is reflected in programming as (decoupled) causal functions on signals: functions whose outputs at time T depend on the history of inputs up to (but not including) T. Alan used these insights to show that FRP primitives such as switching and looping can be encoded in a fairly direct manner via LTL types. In the ensuing Q/A session, it was suggested that “until” may be interpreted in programming as “progress,” and that decidability results for LTL could be leveraged for type checking FRP. Overall, super exciting stuff: this will require some further meditation to internalize and apply!

Over a coffee break, I had a nice conversation with Chris Hawblitzel (MSR Redmond) about our ongoing work on ActionScript, and he was quite happy about the potential for impact in this work. We shared our experiences working with product teams at Adobe and Microsoft.

Next, Benjamin Pierce (UPenn) gave a keynote on CRASH/SAFE, a new collaborative project on building a computer with information-flow safety built in at all levels: hardware, operating system, programming language. In particular, Benjamin went over some interesting design tidbits that showcased what can be conceived and achieved when all legacy constraints are removed: the power and challenges of applying the state-of-the-art with a clean slate.

Over lunch, I was pleasantly surprised to find my undergrad classmate, Akash Lal (who is now at MSR India, and works on concurrency); and I had a long conversation on language design work with Ravi Chugh (who has recently joined Mozilla, and works on type systems). We were joined by Pat Rondon (UCSD, who is the principal driver of the very cool “liquid types” line of work) and Jeff Vaughn (UCLA, who has been working on the now much larger Android security project that we started at UMD).

I skipped the session immediately after lunch to catch up on emails (and some sleep, which, for some reason, always eludes me the first night of a hotel stay).

The last session of the day featured another cool talk on “dependent interoperability”: the basic idea being that it should be possible to mix programs in simply-typed and dependently-typed sublanguages by mediating value-passing at the boundaries, via “boundary terms” that translate values up and down as required, and whose types can be derived by looking at the corresponding constructors for the data types of those values. For example, a library for dependently typed lists would require passing lengths around, and it should be possible to have a simply-typed client use this library by managing lengths on the side. Overall, this seems to mirror hybrid / gradual typing, but is sufficiently intriguing to deserve a deeper look.

POPL begins tomorrow! Eagerly looking forward to a lot of learning throughout the rest of the week. (Our type inference paper will be presented on Friday.)