[TYPES] Poly*, a retargetable polymorphic type system for mobility calculi

[Henning Makholm]

We are pleased to announce the availability of an

            On-line web-accessible demonstration
                 of type inference for Poly*,
  a retargetable polymorphic type system for mobility calculi

Poly* works for process and mobility calculi such as Mobile Ambients
or the pi-calculus. It features a novel form of polymporhism which we
call _spatial polymorphism_. Here the creation of polymorphic variants
is triggered by _movement_ of a mobile entity, in contrast to
traditional notions of polymorphism where variants are created by
let bindings, function application, communication, explicit
instantiation, etc.

Poly* is not a type system but a type system _scheme_; when
instantiated with the reduction axioms for a particular calculus it
automatically derives a type system for it. The on-line demo contains
examples of this for a number of calculi, and also allows the user to
type his own terms and construct his own calculus definitions.


Please find the demo and a technical report that develops the
underlying theory by following the links at

       http://www.macs.hw.ac.uk/DART/software/PolyStar/

Though the demo is fully functional, the graphs it produces will be
scaled to fit in a typical browser window, so large results may not be
readable. For production use or large examples we recommend
downloading the source code for the command-line inference tool and
running it locally.

Do not hesitate to contact us if you have any questions or comments
relating to the system. We would be delighted to receive any feedback
you might happen to think of.

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