The Poly* Type System

This page provides information about the Poly* system. It lists the available resources and it allows a user to easily experiment with a type inference algorithm using an online accessible web demonstration tool. The implementation is also available here to download as a standalone program.

What is Poly* ?

The following notions try to summarize the most important information about the Poly* system:

Poly* is a generic polymorphic type system that makes a sound type system with principal types and with an implemented type inference algorithm for many process calculi.
By generic we mean ranging over many process calculi (expressed by * in the name Poly*).
Poly* employs a generic notion of shape types which describe behavior of processes by a direct description of allowed syntactic configurations.
Meta* is a generic process calculus that can be instantiated by supplying rewriting rules defining an operational semantics to make numerous process calculi such as the π-calculus, the system of Mobile Ambients, and many of their variants.
Poly* provides a type system for any instantiation of Meta*.

Credits and Acknowledgments

The Poly* system was formerly developed by Makholm and Wells based on the previous work on a type system for Mobile Ambients by Amtoft, Makholm, and Wells. Recent updates and extensions of the theory and implementation are due to Jakubův and Wells.

The development of this prototype was funded by EPSRC grant EP/C013573/1 and by EC FP5/FET/GC grant IST-2001-33477 “DART” and supported by Sun Microsystems equipment grant EDUD-7826-990410-US.

Online web demo

You can test the Poly* system and experiment with the type inference algorithm using an online web demonstration of the type inference implementation.

Sebastien Carlier created the Meta* emulator web application which allows a user to simulate rewriting of an input process step by step (currently working only for Mobile Ambients).

Resources

The following list both recent and previous technical reports and conference papers which explain the Poly* theory in details.

We also have a list of common questions about Poly* with answers.

Latest

The latest 2009 technical report contains the most recent updates and extensions of the theory, and a comparison of the expressiveness of shape types and Poly* with related systems. It can be found here:

J. Jakubův and J. B. Wells. The Expressiveness of Generic Process Shape Types, Technical Report TR-HW-MACS-0069, Heriot-Watt University, July 2009.

A previous report and an ESOP'05 paper are available here:

H. Makholm and J. B. Wells. Instant polymorphic type systems for mobile process calculi: Just add reduction rules and close. Technical Report TR-HW-MACS-0022, Heriot-Watt University, November 2004.
H. Makholm and J. B. Wells. Instant polymorphic type systems for mobile process calculi: Just add reduction rules and close. In Programming Languages & Systems, 14th European Symp. Programming, volume 3444 of LNCS, pages 389-407. Springer-Verlag, 2005

Historic

Previous work on the type system PolyA for Mobile Ambients can be found here:

T. Amtoft, H. Makholm, and J. B. Wells. PolyA: True type polymorphism for Mobile Ambients. Technical Report HW-MACS-TR-0015, Heriot-Watt University. February 2004.
H. Makholm and J. B. Wells. Type Inference for PolyA. Technical Report HW-MACS-TR-0013, Heriot-Watt University. January 2004. (This paper is currently the only available description of the details of the type inference algorithm implementation. It describes type inference for PolyA but it applies to Poly* as well.)
T. Amtoft and J. B. Wells. Mobile processes with dependent communication types and singleton types for names and capabilities. Technical Report 2002-3, Kansas State University, Department of Computing and Information Sciences, December 2002. (This is the first paper which describes the “in/open” anomaly.)

Source code download

The source code archive containing the implementation of the type inference algorithm can be downloaded here: polystar-1.42.tar.gz.

To compile the source code you need Moscow ML (with the latest Mar 2008 glibc patch applied) and GNU Make. Moreover to visualize the output of the implementation you might want to use either Graphviz or VCG.