[TYPES] New paper and questions/answers web page for Poly*, a retargetable polymorphic type system for mobility calculi

[Henning Makholm]

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
  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
  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