Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1842/395

Title:  The Polymorphic PiCalculus: Theory and Implementation 
Authors:  Turner , David 
Supervisor(s):  Milner, Robert Doctoral PhD Doctor of Philosophy 
Issue Date:  Jul1996 
Publisher:  University of Edinburgh. College of Science and Engineering. School of Informatics. 
Abstract:  We investigate whether the Picalculus is able to serve as a good foundation for the design and implementation of a stronglytyped concurrent programming language. The first half of the dissertation examines whether the Picalculus supports a simple type system which is flexible enough to provide a suitable foundation for the type system of a concurrent programming language. The second half of the dissertation considers how to implement the Picalculus efficiently, starting with an abstract machine for Picalculus and finally presenting a compilation of Picalculus to C.
We start the dissertation by presenting a simple, structural type system for Picalculus, and then, after proving the soundness of our type system, show how to infer principal types for Piterms. This simple type system can be extended to include useful typetheoretic constructions such as recursive types and higherorder polymorphism. Higherorder polymorphism is important, since it gives us the ability to implement abstract datatypes in a typesafe manner, thereby providing a greater degree of modularity for Picalculus programs.
The functional computational paradigm plays an important part in many programming languages. It is wellknown that the Picalculus can encode functional computation. We go further and show that the type structure of lambdaterms is preserved by such encodings, in the sense that we can relate the type of a lambdaterm to the type of its encoding in the Picalculus. This means that a Picalculus programming language can genuinely support typed functional programming as a special case.
An efficient implementation of Picalculus is necessary if we wish to consider Picalculus as an operational foundation for concurrent programming. We first give a simple abstract machine for Picalculus and prove it correct. We then show how this abstract machine inspires a simple, but efficient, compilation of Picalculus to C (which now forms the basis of the Pict programming language implementation). 
Sponsor(s):  Engineering and Physical Sciences Research Council (EPSRC) 
URI:  http://hdl.handle.net/1842/395 
Appears in Collections:  Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.
