Towards a core calculus for implicitly migration-capable applications

Yitzhak Mandelbaum and I have been thinking about language support for program migration. We submitted a short paper, Towards a core calculus for implicitly migration-capable applications, to PEPM’12 summarizing what we’ve done so far and the direction we’re headed. Here’s the abstract:

Mobile computational devices, like smartphones, tablets and laptops, have become a standard part of the computing landscape. Moreover, many users regularly interact with an assortment of devices, including mobile ones. Therefore, the ability to migrate UI-enabled applications is becoming increasingly important. We describe a design-pattern for applications to simplify support for user-session migration and provide an overview of a lambda calculus for which significant elements of the design pattern can be implemented automatically.

We’d appreciate any ideas, comments, or questions.

ESOP 2011 Papers

I’m happy to announce the final versions of two ESOP 2011 papers. Polymorphic Contracts was work done with João Belo, Atsushi Igarashi, and my advisor, Benjamin Pierce. Measure Transformer Semantics for Bayesian Machine Learning was work done at my internship at MSR Cambridge this summer; the real heroes of this story are Johannes Borgström, Andy Gordon, James Margetson, and Jurgen Van Gael.

See you in Saarbrücken?

Polymorphic Contracts

João Belo, Atsushi Igarashi, Benjamin Pierce, and I submitted a paper, Polymorphic Contracts, to ESOP’11. Here’s the abstract:

Manifest contracts track precise properties by refining types with predicates—e.g., {x:Int | x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give abstract types strong contracts, precisely stating pre- and post-conditions while hiding implementation details—for example, an abstract type of stacks might specify that the pop operation has input type {x:α Stack | not (empty x)}. We formalize this combination by defining FH, a polymorphic calculus with manifest contracts, and establishing its fundamental properties, including type soundness and relational parametricity. Our development relies on a significant technical improvement over earlier presentations of contracts: instead of introducing a denotational model to break a problematic circularity between typing, subtyping, and evaluation, we develop the metatheory of contracts in a completely syntactic fashion, omitting subtyping from the core system and recovering it post facto as a derived property.

Contracts Made Manifest: final version

We’ve sent off the final version of Contracts Made Manifest. There have been quite a few improvements since submission, the most important of which is captured by Figure 1 from our paper:

The axis of blame

Our submission only addressed lax λC, where we had an inexact translation φ into λH and an exact translation ψ out of λH. We show a dual situation for picky λC, where φ is exact and ψ is inexact. Intuitively, languages farther to the right on the “axis of blame” are pickier. Translating from right to left preserves behavior exactly, but left-to-right translations generate terms that can blame more than their pre-images. (There are examples in the paper.) I should note that lax and picky λC seem to be the extremes of the axis of blame: I don’t see a natural way to be laxer than lax λC or pickier than picky λC.

We also show that restricting these calculi to first-order dependency leaves them exactly equivalent; before, we could only show an exact equivalence by eliminating all dependency.

Flapjax: A Programming Language for Ajax Applications

I am immensely pleased to report that our paper on Flapjax was accepted to OOPSLA 2009.

This paper presents Flapjax, a language designed for contemporary Web applications. These applications communicate with servers and have rich, interactive interfaces. Flapjax provides two key features that simplify writing these applications. First, it provides event streams, a uniform abstraction for communication within a program as well as with external Web services. Second, the language itself is reactive: it automatically tracks data dependencies and propagates updates along those data?ows. This allows developers to write reactive interfaces in a declarative and compositional style.

Flapjax is built on top of JavaScript. It runs on unmodi?ed browsers and readily interoperates with existing JavaScript code. It is usable as either a programming language (that is compiled to JavaScript) or as a JavaScript library, and is designed for both uses. This paper presents the language, its design decisions, and illustrative examples drawn from several working Flapjax applications.

The real heroes of this story are my co-authors. Leo, Arjun, and Greg were there for the initial, heroic-effort-based implementation. Jacob and Aleks wrote incredible applications with our dog food. Shriram, of course, saw the whole thing through. Very few of my contributions remain: the original compiler is gone (thank goodness); my thesis work is discussed briefly in How many DOMs? on page 15. Here’s to a great team and a great experience (and a great language)!

Contracts Made Manifest

Benjamin Pierce, Stephanie Weirich, and I submitted a paper to POPL 2010; it’s about contracts. Here’s the abstract:

Since Findler and Felleisen introduced higher-order contracts, many variants of their system have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen in using latent contracts, purely dynamic checks that are transparent to the type system; others use manifest contracts, where refinement types record the most recent check that has been applied. These two approaches are generally assumed to be equivalent—different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding.

Our work extends that of Gronski and Flanagan, who defined a latent calculus \lambda_C and a manifest calculus \lambda_H, gave a translation \phi from \lambda_C to \lambda_H, and proved that if a \lambda_C term reduces to a constant, then so does its \phi-image. We enrich their account with a translation \psi in the opposite direction and prove an analogous theorem for \psi.

More importantly, we generalize the whole framework to dependent contracts, where the predicates in contracts can mention variables from the local context. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of \lambda_C (following Findler and Felleisen’s semantics) and \lambda_H, establish type soundness—a challenging result in itself, for \lambda_H—and extend \phi and \psi accordingly. Interestingly, the intuition that the two systems are equivalent appears to break down here: we show that \psi preserves behavior exactly, but that a natural extension of \phi to the dependent case will sometimes yield terms that blame more because of a subtle difference in the treatment of dependent function contracts when the codomain contract itself abuses the argument.

Edit on 2009-11-03: there’s a newer version, as will appear in POPL 2010.

Edit on 2010-01-22: I have removed the link to the submission, since it is properly subsumed by our published paper.