The Kell Calculus: A Family of Higher-Order Distributed Process Calculi

2005 ◽  
pp. 146-178 ◽  
Author(s):  
Alan Schmitt ◽  
Jean-Bernard Stefani
Keyword(s):  
Higher Order ◽  
Process Calculi ◽  
Distributed Process

scholarly journals An Abstract Machine for a Higher-Order Distributed Process Calculus

2002 ◽  
Vol 66 (3) ◽  
pp. 145-169 ◽  
Author(s):  
Florence Germain ◽  
Marc Lacoste ◽  
Jean-Bernard Stefani
Keyword(s):  
Higher Order ◽  
Process Calculus ◽  
Abstract Machine ◽  
Distributed Process

scholarly journals Bisimulation for Higher-Order Process Calculi

1996 ◽  
Vol 131 (2) ◽  
pp. 141-178 ◽  
Author(s):  
Davide Sangiorgi
Keyword(s):  
Higher Order ◽  
Order Process ◽  
Process Calculi

scholarly journals Recursive equations in higher-order process calculi

2001 ◽  
Vol 266 (1-2) ◽  
pp. 839-852 ◽  
Author(s):  
Mingsheng Ying ◽  
Martin Wirsing
Keyword(s):  
Higher Order ◽  
Order Process ◽  
Process Calculi ◽  
Recursive Equations

Typing and subtyping for mobile processes

1996 ◽  
Vol 6 (5) ◽  
pp. 409-453 ◽  
Author(s):  
Benjamin Pierce ◽  
Davide Sangiorgi
Keyword(s):  
Process Algebra ◽  
Operational Semantics ◽  
Type System ◽  
Higher Order ◽  
Order Process ◽  
Process Calculi ◽  
Mobile Processes

The π-calculus is a process algebra that supports mobility by focusing on the communication of channels. Milner's presentation of the π-calculus includes a type system assigning arities to channels and enforcing a corresponding discipline in their use. We extend Milner's language of types by distinguishing between the ability to read from a channel, the ability to write to a channel, and the ability both to read and to write. This refinement gives rise to a natural subtype relation similar to those studied in typed λ-calculi. The greater precision of our type discipline yields stronger versions of standard theorems on the π-calculus. These can be used, for example, to obtain the validity of β-reduction for the more efficient of Milner's encodings of the call-by-value λ-calculus, which fails in the ordinary π-calculus. We define the syntax, typing, subtyping, and operational semantics of our calculus, prove that the typing rules are sound, apply the system to Milner's λ-calculus encodings, and sketch extensions to higher-order process calculi and polymorphic typing.

scholarly journals A Categorical Axiomatics for Bisimulation

1998 ◽  
Vol 5 (22) ◽  
Author(s):  
Gian Luca Cattani ◽  
John Power ◽  
Glynn Winskel
Keyword(s):  
Higher Order ◽  
Parallel Composition ◽  
Process Algebras ◽  
Process Calculi ◽  
Open Map ◽  
Kleisli Category ◽  
Open Maps

We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. We work with 2-monads, T, on Cat. Operations on processes, such as nondeterministic sum, prexing and parallel composition are modelled using functors in the Kleisli category for the 2-monad T. We may define the notion of open map for any such 2-monad; in examples of interest, that agrees exactly with the usual notion of functional bisimulation. Under a condition on T, namely that it be a dense KZ-monad, which we define, it follows that functors in Kl(T) preserve open maps, i.e., they respect functional bisimulation. We further<br />investigate structures on Kl(T) that exist for axiomatic reasons,<br />primarily because T is a dense KZ-monad, and we study how those structures help to model operations on processes. We outline how this analysis gives ideas for modelling higher order processes. We conclude by making comparison with the use of presheaves and profunctors to model process calculi.

Sign in / Sign up

Export Citation Format

Share Document