TY - CHAP
T1 - Instant polymorphic type systems for mobile process calculi
T2 - 14th European Symposium on Programming, held as part of the Joint European Conferences on Theory and Practice of Software
AU - Makholm, Henning
AU - Wells, J. B.
PY - 2005
Y1 - 2005
N2 - 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 p-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. © Springer-Verlag Berlin Heidelberg 2005.
AB - 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 p-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. © Springer-Verlag Berlin Heidelberg 2005.
UR - http://www.scopus.com/inward/record.url?scp=24644495849&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-31987-0_27
DO - 10.1007/978-3-540-31987-0_27
M3 - Chapter (peer-reviewed)
SN - 978-3-540-25435-5
VL - 3444
T3 - Lecture Notes in Computer Science
SP - 389
EP - 407
BT - Programming Languages and Systems
Y2 - 4 April 2005 through 8 April 2005
ER -