Novel type systems for concurrent programming
languages
GR/L75177
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.
Travel
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.
References
- [1]
-
S. J. Gay.
Some type systems for the pi calculus.
ACM Computing Surveys, 2000.
To appear.
- [2]
-
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.
- [3]
-
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.
- [4]
-
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.