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, volume 3444 of Lecture Notes in Computer Science, pages
389-407 Springer, 2005
A more detailed predecessor is [36]
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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43