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.

Abstract

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)

• Extended Abstract (ps.gz, 280kbytes.) Copyright © 2001 by ACM. This document is posted by permission of ACM and may not be redistributed. See copyright notice.
• Full version (ps.gz, 250kbytes; pdf, 337kbytes.) TCS preprint version. Copyright © 2003 by Elsevier Science. DO NOT REDISTRIBUTE.
• Slides used for an invited talk at FOCLASA2005

$Date: 2005-12-24 00:37:08 +0900 (Sat, 24 Dec 2005) $