Lambda the Ultimate

Java was actually designed to have tuples from the start, but they never quite got in. At one point, I tried to add a tuple-like construct as part of JSR-65. We wanted to extend array initializers to full blown expressions. Eventually, that effort got quashed; I didn’t really resist, since the extension was painful, as such things always are in Java. We should have just done straight tuples as a separate construct - but at the time, that was frowned upon too.

Not surprisingly, Gilad thinks that tuples are great.

Expressing Heap-shape Contracts in Linear Logic, Frances Perry, Limin Jia, David Walker.

Contracts (dynamically checked programmer assertions) are a widely accepted mechanism for specifying, checking and documenting properties of software components. Most, if not all, contract systems expect programmers to use the native programming language to express their program invariants. While this is most effective for many simple invariants, expressing properties of data structures and aliasing patterns can be extremely complicated. If written in the native language in an unstructured way, such contracts are bound to be unclear and ineffective as documentation.

In this paper, we show how to use linear logic as a language of contracts for an imperative programming language. The high-level nature of our linear logical contracts makes specifying memory shape and aliasing properties of complex recursive data structures easy. Moreover, since we give our logic a clear, compositional semantics, the contracts serve as effective, executable documentation for programmer expectations. In order to evaluate the truth of our linear logical contracts at run time, we use a modifed version of LolliMon, a linear logic programming language.

This is a very elegant idea -- write assertions about heap shape using linear logic, and then check those assertions using a logic programming engine that traces the heap.

One thing this work reminds me is that I don't really understand the relationship between the way that they use the "with" connective (A & B) of linear logic and the way conjunction (A /\ B) is used in separation logic.

Is Lua the next big thing (see here for one example)? What's up with that?

If you are in Berkeley on March 15, you can catch Bjarne Stroustrup giving an Outline of C++0x.

If you're not around, you should be able to watch the talk online shortly afterwards.

In the meantime, you can watch videos of recent talks on the Intel Research PL Seminar Series website: Alan Kay, Guy Steele, Bertrand Meyer, Martin Odersky, Hans Boehm, Guido van Rossum...