Lambda the Ultimate

One of the main obstacles for formally verified imperative software is the so called framing problem. A solution to the framing problem has to give a precise answer to the question: "What does a procedure modify and what does in leave unchanged?".

Some weeks ago I have presented the specification view of a new attempt to solve the framing problem (An approach to framing and mutability).

The following paper describes the implementation view of the frame contracts and how the implementation view and the specification view can be kept consistent.

Furthermore it demonstrates how loop invariants can be kept readable by using ghost functions.

Validating LR(1) parsers

An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.

I've always been somewhat frustrated, while studying verified compiler technology, that the scope of the effort has generally been limited to ensuring that the AST and the generated code mean the same thing, as important as that obviously is. Not enough attention has been paid, IMHO, to other compiler phases. Parsing: The Solved Problem That Isn't does a good job illuminating some of the conceptual issues that arise in attempting to take parsers seriously as functions that we would like to compose etc. while maintaining some set of properties that hold of the individuals. Perhaps this work can shed some light on possible solutions to some of those issues, in addition to being worthwhile in its own right. Note the pleasing presence of an actual implementation that's been used on the parser of a real-world language, C99.

One of the annoying/frustrating things about Java's type system is that all reference types are inhabited by null so there's no way to specify, in the type system, that a reference actually refers to an instance and not null. It seems like Haskell's bottom is similar to this.

What are the differences? And where are the type systems that avoid having all types also inhabited by some nullary type?