Project Suggestions in Applied Semantics, 2008-2009

(these will be updated from time to time)

The projects below are outline suggestions - feel free to come and discuss how they could be turned into full proposals, or to suggest others in the same general area. Possible supervisors for these include:

Good typechecking for HOL (Ridge, Owens, Sewell?)

Interactive tools for automated reasoning, such as the HOL4 and Isabelle systems (developed by Mike Gordon and Larry Paulson, with many others), let one write mathematical definitions, type-check them, and support various tactics for automated and manual proof.

The core of this project is the production of a high-quality standalone typechecker for HOL4, that can take a collection of HOL4 source files and quickly do type inference it, with good reporting of any type errors. The HOL4 type system is broadly similar to that of ML, with top-level polymorphism.

Possible approaches are here: SEMINAL: Searching for ML Type-Error Messages Benjamin Lerner, Dan Grossman and Craig Chambers The 2006 ACM SIGPLAN Workshop on ML (ML 2006) Portland, Oregon, 16th September 2006 and here: Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Sci. Comput. Programming, 50:189-224, 2004. Probably one should reuse the existing HOL4 lexing and parsing code.

If the project goes well, a possible extension would be to synthesise, from the typechecked source, Isabelle/HOL or HOL light definitions.

This project would suit a good semantically minded programmer. It would probably be written in OCaml or ML.


Tool support for animating semantics (Gray, Owens?) (Taken?)

Working with realistic programming language type systems or operational semantics is challenging, partly because of the size of the definitions. Better tool support would be very useful, for typesetting, for informal proof, for animation, for use as an oracle for automatic testing of implementations, and for machine-checked proof. We've implemented various partial tools over last few years, leading up to the Ott tool.

This project is to extend Ott with support for animating definitions: taking a term and searching for possible derivations of transitions or typing judgements.

Ott is written in OCaml or ML.


Post-hoc Makefile or Bash semantics (Ridge?)

This project is to produce a post-hoc semantics for the language of Makefiles, or for Bash, and to test it against the implementations.


Peter.Sewell@cl.cam.ac.uk