[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[moca] Poly*, a retargetable polymorphic type system for mobility calculi
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* 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* works for many different mobility calculi; 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
about 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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html