Novel type systems for concurrent programming languages
Final Report

Dr S. J. Gay
Department of Computing Science,
University of Glasgow

Summary of Exceptional Circumstances

Grant GR/L75177 provided £ 51k over three years, starting on 1st October 1997. The principal investigator was Dr Simon Gay. The grant funded a project studentship for Mr Malcom Hole, and provided a budget for travel, equipment and consumables.

The fact that Mr Hole was diagnosed with cancer in March 1999 disrupted work on the project significantly. After an absence of 6 months for treatment, it was felt most appropriate, as Mr Hole was still recovering from radiotherapy, for him to continue his PhD part-time. Furthermore, in December 1999 Dr Gay accepted a position at the University of Glasgow from 27th March 2000. For these reasons, a restructuring of the grant was sought, in order to allow Mr Hole to work part-time over an extended period and to reflect Dr Gay's change of institution. Grant GR/L75177 was therefore terminated on 29th February 2000 and replaced by grant GR/N39494, which subsumes the remaining budget of GR/L75177 and will continue until 31st March 2002. The principal investigator on GR/N39494 is Dr Steve Schneider of Royal Holloway, and Dr Gay is a co-investigator. Although this report is the final report for GR/L75177, it is only an interim report on the project ``Novel Type Systems for Concurrent Programming Languages'', which is continuing under grant GR/N39494.

Project Overview

The aim of the project is to develop new type systems for concurrent programming languages, which allow complex patterns of inter-process communication to be described and specified in a structured way. Theoretical work on the development of such type systems underpins implementation work based on the Pict [3] programming language.

Most of the manpower is provided by Mr Hole, as his PhD thesis will be based on the project work. Dr Gay provides support and collaboration with the theoretical aspects of the project.

Scientific Progress

Please refer to the case for support for a description of the work planned for each task.

Task 1: October 1997-October 1998

Mr Hole spent this period becoming familiar with the p-calculus, type theory, the Pict programming language, and the Pict compiler. Dr Gay was invited to lecture at an EPSRC/LMS MathFIT instructional meeting, held at Imperial College in July 1998, on semantics and type systems for concurrency. A survey article [1] will appear in a special issue of ACM Computing Surveys resulting from this meeting.

Task 2: October 1998-April 1999

Mr Hole produced a modified version of the Pict compiler in which the more complex features of the type system are disabled. This provides a basis for the later addition of session types, before eventually re-integrating higher-order polymorphism. Additionally, this version of Pict supports for ML-style datatype definitions, which are not present in the basic language. This small enhancement of the Pict type system was a preliminary exercise in the kinds of modifications to the compiler which will be necessary later in the project.

During this period we were visited for three months by Emmanuel Coquery, a student from Ecole Normale Supérieure, Paris. In collaboration with Dr Gay, Mr Coquery developed and implemented a novel and efficient algorithm for checking the subtype relation on session types (see Task 3). This algorithm will be useful in implementation work later in the project.

Task 3: October 1997-April 1999

A new approach to session types has been developed by Dr Gay and Mr Hole, which allows correct use of session channels to be enforced by an enhanced type system rather than by syntactic restrictions; in particular, this approach allows session channels to be transmitted from process to process, which was not possible in the original formulation by Honda et al. [4]. As part of the same reformulation, we have added subtyping to the system, and discovered that the combination of subtyping with session types allows client-server protocols to be specified in a concise and flexible way. This theoretical work was presented [2] at the European Symposium on Programming Languages and Systems, held as part of the European Joint Conferences on Theory and Practice of Software, in Amsterdam in March 1999. It will form the basis of later implementation work.

October 1999 onwards

Work has continued on establishing the necessary theoretical properties of the type system developed in Task 3, preparatory to incorporating it into Pict. Work during this period has been slower, as Mr Hole is now working part-time, but is still progressing satisfactorily and a technical report

Additional Work

Dr Gay has formalised the p-calculus and its type system in Isabelle/HOL, an automated theorem-proving system. While not part of the original work plan, this will lead to the capability to construct machine-checked proofs of correctness of the type systems which we are developing for Pict. Working with the new type systems being developed during this project has emphasised the complexity of reasoning about the correctness of type systems. Dr Gay is developing general-purpose techniques for the formalisation of type systems within automatic theorem provers, and hopes that this line of work might form the basis of future research projects.


In April 1998, Mr Hole attended the British Colloquium on Theoretical Computer Science, held at the University of St Andrew's. This was an excellent opportunity for him to hear presentations on a wider range of theoretical computer science topics, and to meet PhD students from other institutions. In May 1998, Mr Hole attended the international conference on Mathematical Foundations of Programming Semantics; the fact that it was held at Queen Mary and Westfield College, London, meant that it was a good opportunity to attend a major conference very cheaply. In March 1999, Mr Hole and Dr Gay attended the European Joint Conferences on Theory and Practice of Software, in Amsterdam, to present a paper on the type system being developed for this project. In September 1999, Dr Gay attended the Banff Higher-Order Workshop, held unusually in Ullapool, Scotland. This meeting was attended by many researchers in automatic theorem proving, and provided valuable feedback on Dr Gay's work on formalisation of type systems.


S. J. Gay. Some type systems for the pi calculus. ACM Computing Surveys, 2000. To appear.

S. J. Gay and M. J. Hole. Types and subtypes for client-server interactions. In S. D. Swierstra, editor, ESOP'99: Proceedings of the European Symposium on Programming Languages and Systems, number 1576 in Lecture Notes in Computer Science, pages 74-90. Springer-Verlag, 1999.

B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. Technical Report CSCI 476, Computer Science Department, Indiana University, 1997. To appear in Proof, Language and Interaction: Essays in Honour of Robin Milner, Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, MIT Press, 1998.

K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In Proceedings of the 6th European Conference on Parallel Languages and Architectures, number 817 in Lecture Notes in Computer Science. Springer-Verlag, 1994.

File translated from TEX by TTH, version 2.78.
On 14 Sep 2001, 14:37.