Types for Concurrent Programming
S. J. Gay
Department of Computer Science
University of London
Egham, Surrey TW20 0EX
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.
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
 was presented at the TACS (Theoretical Aspects
of Computer Software) conference in Sendai, Japan, in September 1997;
the other  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  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  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.
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.
S. Abramsky, S. Gay, and R. Nagarajan.
A type-theoretic approach to deadlock-freedom of asynchronous
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.
S. Abramsky, S. J. Gay, and R. Nagarajan.
A specification structure for deadlock-freedom of synchronous
Theoretical Computer Science, 222(1-2):1-53, 1999.
S. J. Gay.
Some type systems for the pi calculus.
ACM Computing Surveys, 1999.
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.
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
On 14 Sep 2001, 13:47.