Lambda the Ultimate

The 2nd draft of the SPARQL Query Language for the Resource Description Framework (RDF) was published a few days ago by the W3C's RDF Data Access Working Group (DAWG). It's very SQL-like in syntax, but the fact that the data being queried is a graph brings in a raft of issues, as do things like RDF's support for (XML Schema) typed literals alongside named classes/instances. Early implementations include Rasqal (demo - Rasqal's C source, with lots of language bindings) and ARQ for Java. There's a public mailing list for comments.

Once the query language is hammered out then RDF triplestores should make a viable alternative to SQL/RDBMSs, especially for use on the Web and with other 'unstructured' data.

We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotational techniques. The key ingredients are an interpretation of program properties as relations, rather than predicates, and a realization that although many program analyses are traditionally formulated in very intensional terms, the associated transformations are actually enabled by more liberal extensional properties. We illustrate our approach with formal systems for analysing and transforming while-programs. The first is a simple type system which tracks constancy and dependency information and can be used to perform dead-code elimination, constant propagation and program slicing as well as capturing a form of secure information flow. The second is a relational version of Hoare logic, which significantly generalizes our first type system and can also justify optimizations including hoisting loop invariants. Finally we show how a simple available expression analysis and redundancy elimination transformation may be justified by translation into relational Hoare logic.

Not really exciting as such, but this technical report version of the POPL 2004 paper includes most of the proofs, which some might find helpful.