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.

• To develop novel type systems, and novel combinations of existing type systems, for the pi calculus as a prototypical concurrent programming language. These type systems will support static verification of specifications of the communication behaviour of concurrent programs.
• To use the programming language Pict as a vehicle for experiments with the implementation and application of these type systems.

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.

• A reformulation of the theory of session types in the pi calculus, so that session channels can be created and communicated in the same way as standad channels.
• The definition of a notion of subtyping for session types, allowing greater flexibility in the specification and verification of client-server systems.
• The definition of a notion of bounded polymorphism in session types, which we believe to be the first study of any kind of bounded polymorphism in the pi calculus.
• The formalization in Isabelle/HOL of a linear type system for the pi calculus, and a machine-verified proof of type safety.

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.