Programming Tools Group

Research Meetings (Hilary Term 2001)

Topics for Hilary 2001, and before, include:

15 Jan: K. Rustan M. Leino (Compaq SRC) Houdini, an annotation assistant for ESC/Java

ESC/Java is a static program checker for Java, powered by a detailed semantics engine and an automatic theorem prover. It performs modular checking and relies on the programmer to supply light-weight specifications. Houdini is a programming tool built on top of ESC/Java. By inferring many properties of the program, it can be useful as a program checker even in the absence of programmer-supplied specifications.

This talk gives an overview of Houdini and reports on some initial experience with it. (Joint work with Cormac Flanagan.)

22 Jan: Yorck Hunke Dependent Types

Yorck presented some papers on Dependent ML (DML), an extension of ML with a restricted form of dependent types where type checking remains decidable. Types in DML can depend on index objects drawn from a constraint domain, typically natural numbers, and type checking is reduced to constraint satisfaction over linear inequalities. Example DML programs include: array bound check elimination, dead code elimination, capturing invariants of datatypes such as red/black trees.

29 Jan: Kevin Backhouse The Circularity Test for Higher Order Attribute Grammars

Last term, Kevin did some work on the circularity test for traditional attribute grammars. He has found a clean way of specifying and proving the correctness of the algorithm. In today's talk, Kevin gave the group an overview of his proof. He then discussed how the result might be extended to higher order attribute grammars. Higher order AGs are more complicated than standard AGs, because there is no longer a clear distinction between attributes and trees. The circularity test for higher order AGs has to be conservative, because otherwise we cannot guarantee that it will terminate. This is still work in progress, but the group were able to give a lot of useful feedback. Hopefully we will eventually be able to extend the circularity test to cover Eric's IP model.

5 Feb: Research Group Intentional programming: an overview

The group discussed a draft of Oege's lecture for the British Computer Society, resulting in the final text shown here.

12 Feb: Ganesh Sittampalam Incremental Evaluation

Ganesh went through the results of some discussions between Jens-Peter Secher, Oege and himself on how the results of term rewriting could be reused after a small edit to the original term. The conclusions were that we should use a DAG representation to represent sharing not only within a particular term but also the entire rewrite sequence. Maintaining a pointer for each node of the DAG to the first rewrite that makes direct use of that node would allow reuse of at least initial chains of rewrites that were unaffected by the edit.

19 Feb: Research Group A formal model of R5

The group discussed a draft by Eric, Oege and Ganesh of a paper that describes in detail how the IP reduction engine (known as R5) can be modelled as a Haskell program. We identified two major problems with R5 that are solved by the model: copying of subtrees, and the precise meaning of rollback (for dealing with circular attribute dependencies).

26 Feb: David Lacey Binary Decision Diagrams

David showed how you can represent relations over finite domains as BDDs. This can be extended to non-finite domains by adding constraints over the BDD. This method is used in the extended model checker in David's rewrite system.

5 March: Oege de Moor Encoding rewriting transformations in higher-order attribute grammars

We described a general method of encoding a set of rewrite rules as attribution functions in a higher-order attribute grammar. The method is inspired by the Hoffmann-O'Donnell algorithm for matching a large set of patterns against a tree.

12 March: Eric Van Wyk Program analysis and transformation via model checking

Eric gave parts of his talk "Program analysis and transformation via model checking" and we discussed what examples where most interesting and the best methods for presenting them to an audience.