A Generic Type System for the Pi-Calculus

By Atsushi Igarashi and Naoki Kobayashi. Theoretical Computer Science, 311(1-3):121-163, January 2004.

An extended abstract appeared in Proceedings of ACM Symposium Conference on Principles of Programming Languages (POPL), pages 128-141, London, England, January 2001.


We propose a general, powerful framework of type systems for the π-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like deadlock-freedom and race-freedom. A key idea is to express types and type environments as abstract processes: We can check various properties of a process by checking the corresponding properties of its type environment. The framework clarifies the essence of recent complex type systems, and it also enables sharing of a large amount of work such as a proof of type preservation, making it easy to develop new type systems.

PostScript/pdf file(s)