The Polymorphic Pi-calculus Theory and Implementation David N …

Short Description
A theory of bisimulation for the ?-calculus. Techni-. cal Report ECS-LFCS-93-270, Laboratory for Foundations of Com-. puter Science, University of Edinburgh …

Website: www.lfcs.inf.ed.ac.uk | Filesize: 1197kb

Content
The Polymorphic Pi-calculus:
Theory and Implementation
David N. Turner
Ph. D.
University of Edinburgh
1995Abstract
We investigate whether the -calculus is able to serve as a good foundation for
the design and implementation of a strongly-typed concurrent programming language.
The rst half of the dissertation examines whether the -calculus 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 -calculus eciently, starting
with an abstract machine for -calculus and nally presenting a compilation of
-calculus to C.
We start the dissertation by presenting a simple, structural type system for
-calculus, and then, after proving the soundness of our type system, show how
to infer principal types for -terms. This simple type system can be extended
to include useful type-theoretic constructions such as recursive types and higherorder
polymorphism. Higher-order polymorphism is important, since it gives
us the ability to implement abstract datatypes in a type-safe manner, thereby
providing a greater degree of modularity for -calculus programs.
The functional computational paradigm plays an important part in many programming…