ﻻ يوجد ملخص باللغة العربية
Besides respecting prescribed protocols, communication-centric systems should never get stuck. This requirement has been expressed by liveness properties such as progress or (dead)lock freedom. Several typing disciplines that ensure these properties for mobile processes have been proposed. Unfortunately, very little is known about the precise relationship between these disciplines--and the classes of typed processes they induce. In this paper, we compare L and K, two classes of deadlock-free, session typed concurrent processes. The class L stands out for its canonicity: it results naturally from interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashis usage types, includes processes not typable in other type systems. We show that L is strictly included in K. We also identify the precise condition under which L and K coincide. One key observation is that the degree of sharing between parallel processes determines a new expressiveness hierarchy for typed processes. We also provide a type-preserving rewriting procedure of processes in K into processes in L. This procedure suggests that, while effective, the degree of sharing is a rather subtle criteria for distinguishing typed processes.
Types in logic programming have focused on conservative approximations of program semantics by regular types, on one hand, and on type systems based on a prescriptive semantics defined for typed programs, on the other. In this paper, we define a new
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running
Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between session typ
We show that the techniques for resource control that have been developed in the so-called light logics can be fruitfully applied also to process algebras. In particular, we present a restriction of Higher-Order pi-calculus inspired by Soft Linear Lo
There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics. Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong