[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[moca] New paper and questions/answers web page for Poly*, a retargetable polymorphic type system for mobility calculi
About a month ago, we announced a web interface for experimenting with
type inference in Poly*, a retargetable polymorphic type system for
mobility calculi.
We would now like to announce that we have since then added these 3
items to the Poly* web page:
(1) A list of common questions about Poly* with answers.
(2) The ESOP '05 conference paper on Poly*.
(3) The long technical report on Poly*.
The Poly* web page is at:
http://www.macs.hw.ac.uk/DART/software/PolyStar/
The list (1) contains these questions and their answers:
* What is the expressive power of the restricted portion of Poly*
that has principal typings?
* What is the complexity of your type checking and type inference?
* Is there a connection with ambient logic and logics for XML?
* Wouldn't what you are doing be better done as abstract
interpretation?
* Why does the type system not reject malformed terms?
* Your approach looks too much like data flow analysis. Why do you
say you are doing types?
* Can the D-pi calculus be represented within Meta*?
* Why doesn't Poly* have a safety result with respect to some
specific property? Can it be a type system without such a result?
* But your types look too much like processes! How can you call them
types?
We've put these questions and answers on this web page mainly because
they are much too long to fit in a conference paper and also they are
of general interest to all our future work on Poly*.
The ESOP '05 paper (2) is this:
Henning 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,
LNCS. Springer-Verlag, 2005.
Abstract:
Many different mobile process calculi have been invented, and for
each some number of type systems has been developed. Soundness and
other properties must be proved separately for each calculus and
type system. We present the generic polymorphic type system Poly*
which works for a wide range of mobile process calculi, including
the pi-calculus and Mobile Ambients. For any calculus satisfying
some general syntactic conditions, well-formedness rules for types
are derived automatically from the reduction rules and Poly* works
otherwise unchanged. The derived type system is automatically sound
(i.e., has subject reduction) and often more precise than previous
type systems for the calculus, due to Poly*'s spatial polymorphism.
We present an implemented type inference algorithm for Poly* which
automatically constructs a typing given a set of reduction rules and
a term to be typed. The generated typings are principal with
respect to certain natural type shape constraints.
The ESOP '05 paper has significant simplifications from all earlier
versions and many more examples. If you have tried reading any
earlier versions, and found them a bit difficult, we think you may
enjoy reading this paper instead.
The technical report (3) has the same authors and title. Its
advantage is that it is a long technical report with more text and
also has extra sections describing features not in the ESOP '05 paper.
Its disadvantage is that it was finished earlier than the ESOP '05
paper, and does not have the simplifications and additional examples.
--
Henning Makholm The development of Poly* and its implementation was
Joe Wells funded by EC FP5/IST/FET grant IST-2001-33477 "DART"
Heriot-Watt University
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html