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