Types for Concurrent Programming
(SCI/180/96/155/G)
Final Report

S. J. Gay
Department of Computer Science
Royal Holloway, University of London
Egham, Surrey TW20 0EX

Summary

During the period of the grant I have studied the foundations of concurrent programming languages, i.e. languages for programming systems consisting of independent yet communicating components. My research has focused on the use of types, which can be thought of as succinct and automatically verifiable specifications, to describe the communication behaviour of concurrent programs. I have developed a type system which allows several standard Internet protocols to be specified in a flexible and novel way. The grant itself has enabled me to attend a number of UK and international conferences, both to present papers and more generally to maintain contact with the research community.

Work Done

The grant has supported my continuing work in the area of type systems for concurrent programming languages. Initially, I prepared the final versions of two papers on interaction categories, a foundational framework for type systems in concurrency. One paper [1] was presented at the TACS (Theoretical Aspects of Computer Software) conference in Sendai, Japan, in September 1997; the other [2] has now appeared in Theoretical Computer Science. I then switched attention to the development of novel type systems for programming languages based on the pi calculus. Working with a PhD student, I have developed a type system which allows communication protocols, for example standard Internet protocols such as POP3, to be specified in a succinct and automatically verifiable manner. The main novelty of this system is the way in which subtyping allows the server side of a protocol to be enhanced while maintaining compatibility with existing clients. A paper describing this work [4] was presented at the European Symposium on Programming Languages and Systems in Amsterdam, in March 1999. My PhD student is now working on implementing this type system as an extension to the Pict programming language. A prototype type checker has been implemented by a MSc student from Ecole Normale Supérieure, Paris, who visited me from January to April 1999.

In 1998 I was invited to lecture at an EPSRC/LMS MathFIT instructional meeting on types and semantics for concurrency. An accompanying survey article [3] will appear in ACM Computing Surveys. I have also give seminars at Leicester University and Edinburgh University, and have spoken at the Imperial College workshop on Theory and Formal Methods of Computing.

The main difference between the work originally proposed and the work carried out is that I have de-emphasised the interaction categories approach to concurrent types in favour of a more operational approach directly based on the pi calculus. The reason for this is that the interaction categories framework has never been able to account well for mobility, which is an important feature of interesting concurrent systems. The pi calculus based work hsa been very successful, justifying this decision.

Follow-on Grants

During the period of the grant, I applied for and received EPSRC funding for a PhD student, who is now working with me in the same area. My work with type systems for the pi calculus has led me to begin investigation of automatic theorem-proving technology and its application to reasoning about correctness of type systems. During the next year I hope to apply for an EPSRC grant to continue this line.

Publications

[1]
S. Abramsky, S. Gay, and R. Nagarajan. A type-theoretic approach to deadlock-freedom of asynchronous systems. In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software. International Symposium TACS'97, number 1281 in Lecture Notes in Computer Science, pages 295-320, Sendai, Japan, September 1997. Springer-Verlag.

[2]
S. Abramsky, S. J. Gay, and R. Nagarajan. A specification structure for deadlock-freedom of synchronous processes. Theoretical Computer Science, 222(1-2):1-53, 1999.

[3]
S. J. Gay. Some type systems for the pi calculus. ACM Computing Surveys, 1999. To appear.

[4]
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.

Expenditure

I originally applied for £ 4000, of which £ 1000 was to be used for purchase of computing equipment and £ 3000 for travel. The grant I received was for £ 3000. However, it turned out to be unnecessary for me to spend money on equipment as it was provided instead by my department, and therefore I had the travel budget which I had requested. Apart from a small sum for purchase of proceedings of conferences which I did not attend, I have spent all of the grant on travel, as detailed below.
September 1997
£ 1466 for attendance (travel, registration and subsistence) at the TACS (Theoretical Aspects of Computer Software) conference in Sendai, Japan. A co-authored paper was presented at this conference.
April 1998
£ 317 for attendance (travel, registration and subsistence) at the BCTCS (British Colloquium in Theoretical Computer Science) conference in St. Andrew's.
May 1998
£ 250 for attendance (registration and subsistence) at the Imperial College workshop on Theory and Formal Methods in Bath. I gave a talk at this meeting.
May 1998
£ 114 for attendance (registration and travel) at the MFPS (Mathematical Foundations of Programming Semantics) conference in London. This was an opportunity to attend a major international conference very cheaply.
July 1998
£ 34 for purchase of two volumes of proceedings from previous LICS (Logic in Computer Science) conferences.
December 1998
£ 65 towards the cost of a visit to the University of Edinburgh, where I gave a seminar and spent two days in discussions with several members of the Computer Science department. Most of the cost was met by Edinburgh.
December 1998
£ 62 for attendance at a British Computer Society meeting on Formal Aspects of Computer Science, in London.
March 1999
£ 692 for attendance (travel, registration and subsistence) at the European Symposium on Programming Languages and Systems in Amsterdam. I presented a paper, co-authored with my PhD student, at this conference.



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