Project Suggestions in Applied Semantics, 2005-2006

(these will be updated from time to time)

Peter Sewell

Tool support for semantics

Project description:

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, so there are lots of ideas.

Some notes on desirable features are available on request, and the POPLmark challenge paper is also relevant.

Most of the system would probably be best written in OCaml or ML.

Special resources:

Post-hoc Makefile or Bash semantics

Project description:

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

Special resources:

Acute runtime implementation

Project description:

A group of us have developed the experimental programming language acute for high-level distributed programming. The language has a complete formal definition and an implementation (in Fresh OCaml). The runtime is essentially an interpreter operating over the abstract syntax (extended with closures and explicit representations of evaluation contexts).

This project is to implement a more efficient runtime for all or part of the language. Particularly interesting would be to target the OCaml bytecode, or a mild variation thereof.

Special resources:

TCP - model implementation and flow-control parameterisation

Project description:

We've produced a post-hoc specification of TCP - as it is actually implemented. The specification is expressed in Higher-Order Logic (with the HOL tool); it's validated against the behaviour of linux, BSD and WXP stacks. This project would involve writing a clean implementation of TCP based on our spec (with code structured for clarity rather than maximum speed), likely in OCaml. Initially it could be run purely in userspace (we have OCaml libraries for packet injection and monitoring that could be used); perhaps later it could be tied in with the linux or BSD sockets interface. If the project goes well, an interesting extension would be to refactor the code to enable the existing congestion control algorithms to be smoothly replaced by recently-proposed alternatives - congestion marking, etc.

Special resources:

For the later parts: a linux or BSD machine; some test environment.

A debian apt-undo

Project description:

Package management operations really should support an undo operation. Details to be discussed.

Special resources:

Distributed Infrastructure above the TCP/UDP/Sockets semantics

Project description:

This project is to select and implement some interesting distributed algorithms, above our OCaml language binding for the modelled sockets primitives, using our TCP semantics as an informal reference. Candidate algorithms include peer-to-peer algorithms such as Chord or Pastry, or randomized algorithms such as van Renesse's Gossip-style Failure Detection Service.

Special resources: