[TYPES] New paper and questions/answers web page for Poly*,
a retargetable polymorphic type system for mobility calculi
henning at makholm.net
Thu Jan 13 16:40:16 EST 2005
About a month ago, we announced a web interface for experimenting with
type inference in Poly*, a retargetable polymorphic type system for
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:
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
* 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
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.
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
star 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 star 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
star 's spatial polymorphism. We present an implemented type
inference algorithm for Poly star 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
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"
More information about the Types-list