Novel Type Systems for Concurrent Programming Languages

Funding

This project began in October 1996, with 51000 of funding from the EPSRC, when I was in the Department of Computer Science at Royal Holloway, University of London.

Originally known as GR/L75177, the grant was terminated as a result of my move to Glasgow in 2000, and replaced by GR/N39494, held jointly with Steve Schneider at Royal Holloway. The project ended on 31 December 2002.

Personnel

Malcolm Hole was funded by a project studentship attached to this grant, and the results of the project will form the basis of his PhD thesis.

Goals

The original grant application is available as PDF. The goals of the project were as follows.

As the project progressed, the emphasis shifted from implementation work based on Pict, to theoretical investigation of subtyping for session types in pi calculus.

Also, our experience of carrying out lengthy proofs of type safety by hand led to an investigation of the application of automatic theorem-proving technology to reasoning about pi calculus type systems.

Results

The main achievements of the project are as follows.

The following publications have been produced.

S. J. Gay and M. Hole. Types and Subtypes for Client-Server Interactions.
In: Proceedings of the European Symposium on Programming Languages and Systems. Springer-Verlag LNCS 1576, 1999.
Available as PostScript.
S. J. Gay and M. Hole. Types for Correct Communication in Client-Server Systems.
Technical report CSD-TR-00-07, Department of Computer Science, Royal Holloway, University of London, 2000.
Available as PostScript.
S. J. Gay. A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL.
In: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001).
Springer-Verlag LNCS series, 2001. Copyright Springer-Verlag.
Available as PostScript. Isabelle sources are here.
S. J. Gay and M. Hole. Types and Subtypes for Correct Communication in Client-Server Systems.
Technical report TR-2003-131, Department of Computing Science, University of Glasgow, February 2003.
Available as PDF.
M. Hole and S. J. Gay. Bounded Polymorphism in Session Types.
Technical report TR-2003-132, Department of Computing Science, University of Glasgow, March 2003.
Available as PDF.

Malcolm Hole's PhD thesis will be submitted during 2003.

An intermediate report on the project (actually the final report on the original grant) is available as PDF and HTML. A short summary of results (up to May 2000) is also available as PDF and HTML.

The final report on the project is available as PDF.