POPL 2012: 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages

TutorialFest!

The POPL 2012 TutorialFest contains no less than seven tutorials, covering a variety of topics. The tutorials will be held on January 28, immediately following the main POPL conference. A separate TutorialFest registration is required.

Registrants of TutorialFest may attend any of the tutorials offered throughout the day. (This allows following four tutorials in full.) To keep costs down, no meals are included.

Most tutorials will be held twice during the day, giving attendees plenty of options for scheduling. This year, POPL is favouring a "distilled tutorial format": each tutorial will be 90 minutes, rather than a half day.

Early tutorial registration fee is $60 for students, $90 for SIGPLAN and/or ACM members and $120 for all others.

Late tutorial registration fee is $80 for students, $120 for SIGPLAN and/or ACM members and $150 for all others.

Note that registration gives access to all tutorials, you don't need to register separately for each tutorial.

Juliusz Chroboczek, Universite de Paris-Diderot (Paris 7), Paris, France
- Serialising a concurrent program using continuation-passing style
  [Show details]
  
  Abstract: In this tutorial, I will show how a program using threads can be transformed in a systematic manner into an event-driven program that is, in a suitable sense, equivalent to the initial program. I will start by giving some background about concurrent programming, threads and event-driven programming. I will then give an example of a threaded program that is not completely trivially written in a sequential form; I will then manually transform it into an event-driven program.
  
  No specific knowledge will be required, except for a passing familiarity with threads. While the presented techniques are language-agnostic, the tutorial will be given in Scheme (I will give a quick reminder about Scheme's syntax).
  
  Bio: Juliusz Chroboczek is a lecturer at the University of Paris-Diderot (Paris 7).

Byron Cook, Microsoft Research, Cambridge and Queen Mary, University of London

Proving program termination and liveness
[Show details]

William Cook, University of Texas, Austin

Build your own partial evaluator in 90 minutes
[Show details]

Martin Escardo, University of Birmingham

Seemingly impossible functional programs
[Show details]

Abstract: Programming language semantics is typically applied to prove compiler correctness and allow (manual or automatic) program verification. Certain kinds of semantics can also be applied to discover programs that one wouldn't have otherwise thought of. This is the case, in particular, for semantics that incorporate topological ingredients (limits, continuity, openness, compactness). For example, it turns out that some function types (X -> Y) with X infinite (but compact) do have decidable equality, contradicting perhaps popular belief, but certainly not (higher-type) computability theory. More generally, one can often check infinitely many cases in finite time.

I will show you such programs, run them fast in surprising instances, and introduce the theory behind their derivation and working. In particular, I will study a single (very high type) program that (i) optimally plays sequential games of unbounded length, (ii) implements the Tychonoff Theorem from topology (and builds finite-time search functions for infinite sets), (iii) realizes the double-negation shift from proof theory (and allows us to extract programs from classical proofs that use the axiom of countable choice). There will be several examples in the languages Haskell and Agda.

Learning objectives: After attending the tutorial, a student will understand topology in both denotational and operational semantics, its application to programming, and an overview of its fundamental connections with higher-type computability theory, game theory and proof theory.

Bio: Martin Escardo's first degree was from UFRGS, Brazil, where he also got an MSc by research. During his studies, he worked in industry. He then joined Imperial College in 1993 for his PhD under the supervision of M.B. Smyth. After completing this, he was a postdoc at Imperial, a lecturer at the Universities of Edinburgh and St Andrews in Scotland. He then joined the University of Birmingham in England, and was appointed as a Reader in 2006. He has worked on exact real number computation, semantics, topology, higher-type computability, constructive mathematics, proof theory and their connections.

Andreas Gal, Mozilla

Compiling the Web
[Show details]

Rustan Leino, Microsoft Research

Using Chalice to reason about objects and concurrency
[Show details]

Abstract: A long-standing dream, program verification has got a lot of traction in the last decade, in which there has been a surge of research around, for example, specification methodologies, verification engines, and SMT solvers. Chalice is a programming language and a program verifier aimed mostly at two difficult verification tasks: objects in the heap and concurrent threads of control. The reasoning model in Chalice associates with each memory resource a set of permissions. The permissions, which control what a thread can do at any given time, can be transferred between threads and can be stored in the heap. This reasoning model, which is known as implicit dynamic frames with fractional permissions, yields a flexible way to specify and verify correctness properties of programs.

In this tutorial, I will present Chalice and its reasoning model through a series of program examples. Features covered include pre- and postconditions, shared memory, locks, monitor invariants, deadlock prevention, and channels. I will also describe how the Chalice model is encoded in the Boogie intermediate verification language, from which first-order verification conditions are generated and fed to an SMT solver.

Chalice is joint work with Stefan Heule, Peter Müller, Jan Smans, and Alex Summers.

Learning objectives: After attending the tutorial, a student will know how to use Chalice to verify simple concurrent programs, will understand the "implicit dynamic frames with fractional permissions" reasoning model in Chalice, and will have some idea of how to build or extend a program verifier like Chalice.

Bio: Rustan Leino is a Principal Researcher at Microsoft Research. He is known for his work on programming methods and verification tools, which includes ESC/Java, Spec#, Boogie, Dafny, and Chalice. Before his PhD (Caltech, 1995), Leino was a developer and technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner video blog on channel9.msdn.com. In his spare time, he plays music and teaches cardio exercise classes.

Peter O'Hearn, Queen Mary, University of London

Separation Logic
[Show details]

Abstract: Separation logic is an extension of Hoare's logic for reasoning about programs that manipulate pointers. Its assertion language extends classical logic with a separating conjunction operator A * B, which asserts that A and B hold for separate portions of memory. In this tutorial I will first cover the basics of the logic, concentrating on highlights from the early work.

The separating conjunction fits together with inductive definitions in a way that supports natural descriptions of mutable data structures.
Axiomatizations of pointer operations support in-place reasoning, where a portion of a formula is updated in place when passing from precondition to postcondition, mirroring the operational locality of heap update.
Frame axioms, which state what does not change, can be avoided when writing specifications.
The formalism supports local reasoning, where specifications and proof can concentrate on a program's footprint (the cells it touches) rather than tracking the entire global state of a system.

These points together enable specifications and proofs for pointer programs that are dramatically simpler than was possible previously, in many cases approaching the simplicity associated with proofs of pure functional programs. I will describe how that is, and where rough edges lie (programs whose proofs are still more complex than we would like).

Then, after the basic part, I will discuss how these points 1-4 feed into research on mechanized verification, both for interactive proof in proof assistants and for automatic proof and abstract interpretation.

Bio: Peter's research interests are in logic and semantics of computation. With John Reynolds, he developed separation logic, and with David Pym, bunched logic, a general logic of resource, which is a more abstract cousin of and precursor to separation logic. He has also proposed a concurrent separation logic (proven sound by Steve Brookes), which has made inroads on the problem of modular reasoning about shared-memory concurrent programs.

Peter received his PhD from Queen's University in Kingston, Canada, in 1991 and was on faculty at Syracuse University until 1996, when he moved to Queen Mary, University of London, where he is a Professor of Computer Science. In 2007 Peter received a Royal Society Wolfson Research Merit Award. In 2011 he received the Most Influential POPL Paper Award, given annually for a paper published at the POPL symposium 10 years earlier, for the paper BI as an Assertion Language for Mutable Data Structures.