Lambda the Ultimate

This link describes an implementation of dimensional analysis in C++ using the Boost MPL. What this means is that physical quantities have a type parametrised by a tuple of integers representing the order of physical dimension (i.e. mass, length, time, etc...) with rules determining what operations can be carried out. This is a standard sanity check for equations in physics and easily catches typos.

For example the equation for the force acting on two massive bodies is G(m₁m₂)/d². If this were accidentally entered as force f = G*(m1+m2)/(d*d) (perhaps due to misremembering the formula) the compiler would throw a type error.

This is clearly a useful techniques for say, rocket guidance systems. What other languages are capable of doing this without having to declare a morass of types and functions relating those types to each other?

Shape analysis for composite data structures. MSR-TR-2007-13.

We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include ``cyclic doubly-linked lists of acyclic doubly-linked lists'', ``singly-linked lists of cyclic doubly-linked lists with back-pointers to head nodes'', etc. The analysis introduces the use of generic higher-order inductive predicates describing spatial relationships together with a method of synthesizing new parametrized spatial predicates which can be used in combination with the higher-order predicates. In order to evaluate the proposed approach for realistic programs we have implemented the analysis and performed experiments with it on examples drawn from device drivers. During our experiments the analysis proved the memory safety of several routines belonging to an IEEE 1394 (firewire) driver, and also found several previously unknown memory safety bugs and memory leaks. To our knowledge this represents the first known successful application of shape analysis to non-trivial systems-level code.

Seems relevant to some of the discussions currently going on (e.g., how PLT can help practitioners).

The analysis described in this paper fits in to the common structure of shape analyses, and is based on abstract interpretation.