A partially deadlock-free typed process calculus
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 128-139
- https://doi.org/10.1109/lics.1997.614941
Abstract
We propose a novel static type system for a process calculus, which ensures both partial deadlock-freedom and partial confluence. The key novel ideas are: (1) introduction of the order of channel use as type information and (2) classification of communication channels into reliable and unreliable channels based on their usage and a guarantee of the usage by the type system. We can ensure that communication on reliable channels never causes deadlock and also that certain reliable channels never introduce nondeterminism. With the type system, for example, the simply typed /spl lambda/-calculus can be encoded into the deadlock-free and confluent fragment of our process calculus; we can therefore recover behavior of the typed /spl lambda/-calculus in the level of process calculi. We also show that typical concurrent objects can also be encoded into the deadlock-free fragment.Keywords
This publication has 9 references indexed in Scilit:
- A calculus of mobile processes, IPublished by Elsevier ,2004
- Typing and subtyping for mobile processesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Linearity and the pi-calculusPublished by Association for Computing Machinery (ACM) ,1996
- Concurrent HaskellPublished by Association for Computing Machinery (ACM) ,1996
- On reduction-based process semanticsTheoretical Computer Science, 1995
- Concurrent objects in a process calculusPublished by Springer Nature ,1995
- Toward Foundations of Concurrent Object‐Oriented Programming‐Types and Language DesignTheory and Practice of Object Systems, 1995
- Logic Programming in a Fragment of Intuitionistic Linear LogicInformation and Computation, 1994
- The Polyadic π-Calculus: a TutorialPublished by Springer Nature ,1993