Ezra's Research

At the Oregon Summer School 2006, Robert Harper presented his Lambda 5, a modal-logic-as-distributed-programming-language. The idea here was that modal logic allows you to reason about things that are true in some "possible world"—and since, via Curry-Howard, true statements are like types of values that are known to exist, the programming-language interpretation of "proposition true at a possible world" is "data available at a possible world"; Harper et al. interpret a "possible world" as a node on a network. Thus, Lambda 5 gives you a way to write terms that are local or mobile: you create local values by publishing an address, which others can use; you create mobile values by packaging them up in a context-independent way. You consume the latter by simply "unboxing" them. The address of a local value is harder to consume—you need to use a binding construct whose body is executed in a hypothetical world where only the addressed value is available.

Harper's presentation was fast & furious, and if you weren't already adept with propositions-as-types, you were probably lost at the beginning. I held on with my toes. Afterward, I got the paper [1, 2] and have been looking at it, trying to figure out if it's going to help me with the issues of locality and distribution that I've been dealing with in the context of Links.

There's an important drawback, or at least caveat, about Lambda 5 as a theoretical approach to distributed computing. It explicitly avoids issues of concurrency. The entire multi-node network of locations is assumed to have a single thread of control. When you consider that there is a substantial bulk of research called "Distributed Computing" and that this research is almost all primarily concerned with issues of concurrency, you might consider this omission rather serious. In the second paper [2], Harper and company use letcc to make control flow explicit, arguing that this gives a way to recover concurency. But if I understand what they're doing, it amounts to a kind of explicit, cooperative multi-tasking—a poor approximation to the situation (and the problems) of distributed systems. My question for this line of research: What are you trying to accomplish?