A generic type system for the Pi-calculus

13 years 6 months ago
A generic type system for the Pi-calculus
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 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.
Atsushi Igarashi, Naoki Kobayashi
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2001
Where POPL
Authors Atsushi Igarashi, Naoki Kobayashi
Comments (0)