Lambda the Ultimate

Since discussions about the appropriateness of policy enforcement have already arisen, I'd like to suggest that in future, such comments be posted to this thread, or as appropriate, to another thread in this forum (i.e. the Site Operation Discussions forum).

Topics and comments posted in this forum won't appear on the RSS feeds of those who have chosen only to subscribe to the home page or the main discussion forum. The earlier LtU: Policies Document topic was posted to the home page, and its discussion was getting long.

Abstracting Allocation: The New new Thing. Nick Benton.

We introduce a Floyd-Hoare-style framework for specification and verification of machine code programs, based on relational parametricity (rather than unary predicates) and using both step-indexing and a novel form of separation structure. This yields compositional, descriptive and extensional reasoning principles for many features of low-level sequential computation: independence, ownership transfer, unstructured control flow, first-class code pointers and address arithmetic. We demonstrate how to specify and verify the implementation of a simple memory manager and, independently, its clients in this style. The work has been fully machine-checked within the Coq proof assistant.

This is, of course, related to TAL, PCC etc. If you find the deatils too much, I suggest reading the discussion (section 7) to get a feel for the possible advantages of this approach.