Instant polymorphic type systems for mobile process calculi: Just add reduction rules and close

Henning Makholm, J. B. Wells

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

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

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings
Pages389-407
Number of pages19
Volume3444
ISBN (Electronic)978-3-540-31987-0
DOIs
Publication statusPublished - 2005
Event14th European Symposium on Programming, held as part of the Joint European Conferences on Theory and Practice of Software - Edinburgh, United Kingdom
Duration: 4 Apr 20058 Apr 2005

Publication series

NameLecture Notes in Computer Science
Volume3444
ISSN (Print)0302-9743

Conference

Conference14th European Symposium on Programming, held as part of the Joint European Conferences on Theory and Practice of Software
Abbreviated title ESOP 2005 and ETAPS 2005
CountryUnited Kingdom
CityEdinburgh
Period4/04/058/04/05

Fingerprint Dive into the research topics of 'Instant polymorphic type systems for mobile process calculi: Just add reduction rules and close'. Together they form a unique fingerprint.

  • Cite this

    Makholm, H., & Wells, J. B. (2005). Instant polymorphic type systems for mobile process calculi: Just add reduction rules and close. In Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings (Vol. 3444, pp. 389-407). (Lecture Notes in Computer Science; Vol. 3444). https://doi.org/10.1007/978-3-540-31987-0_27