ترغب بنشر مسار تعليمي؟ اضغط هنا

On sequentiality and well-bracketing in the $pi$-calculus

125   0   0.0 ( 0 )
 نشر من قبل Daniel Hirschkoff
 تاريخ النشر 2021
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

The $pi$ -calculus is used as a model for programminglanguages. Its contexts exhibit arbitrary concurrency, makingthem very discriminating. This may prevent validating desir-able behavioural equivalences in cases when more disciplinedcontexts are expected.In this paper we focus on two such common disciplines:sequentiality, meaning that at any time there is a single threadof computation, and well-bracketing, meaning that calls toexternal services obey a stack-like discipline. We formalise thedisciplines by means of type systems. The main focus of thepaper is on studying the consequence of the disciplines onbehavioural equivalence. We define and study labelled bisim-ilarities for sequentiality and well-bracketing. These relationsare coarser than ordinary bisimilarity. We prove that they aresound for the respective (contextual) barbed equivalence, andalso complete under a certain technical condition.We show the usefulness of our techniques on a number ofexamples, that have mainly to do with the representation offunctions and store.



قيم البحث

اقرأ أيضاً

156 - Kirstin Peters 2014
We study whether, in the pi-calculus, the match prefix-a conditional operator testing two names for (syntactic) equality-is expressible via the other operators. Previously, Carbone and Maffeis proved that matching is not expressible this way under ra ther strong requirements (preservation and reflection of observables). Later on, Gorla developed a by now widely-tested set of criteria for encodings that allows much more freedom (e.g. instead of direct translations of observables it allows comparison of calculi with respect to reachability of successful states). In this paper, we offer a considerably stronger separation result on the non-expressibility of matching using only Gorlas relaxed requirements.
Formalising the pi-calculus is an illuminating test of the expressiveness of logical frameworks and mechanised metatheory systems, because of the presence of name binding, labelled transitions with name extrusion, bisimulation, and structural congrue nce. Formalisations have been undertaken in a variety of systems, primarily focusing on well-studied (and challenging) properties such as the theory of process bisimulation. We present a formalisation in Agda that instead explores the theory of concurrent transitions, residuation, and causal equivalence of traces, which has not previously been formalised for the pi-calculus. Our formalisation employs de Bruijn indices and dependently-typed syntax, and aligns the proved transitions proposed by Boudol and Castellani in the context of CCS with the proof terms naturally present in Agdas representation of the labelled transition relation. Our main contributions are proofs of the diamond lemma for residuation of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions.
We study the relation between process calculi that differ in their either synchronous or asynchronous interaction mechanism. Concretely, we are interested in the conditions under which synchronous interaction can be implemented using just asynchronou s interactions in the pi-calculus. We assume a number of minimal conditions referring to the work of Gorla: a good encoding must be compositional and preserve and reflect computations, deadlocks, divergence, and success. Under these conditions, we show that it is not possible to encode synchronous interactions without introducing additional causal dependencies in the translation.
86 - Rob van Glabbeek 2018
Process calculi may be compared in their expressive power by means of encodings between them. A widely accepted definition of what constitutes a valid encoding for (dis)proving relative expressiveness results between process calculi was proposed by G orla. Prior to this work, diverse encodability and separation results were generally obtained using distinct, and often incompatible, quality criteria on encodings. Textbook examples of valid encoding are the encodings proposed by Boudol and by Honda & Tokoro of the synchronous choice-free $pi$-calculus into its asynchronous fragment, illustrating that the latter is no less expressive than the former. Here I formally establish that these encodings indeed satisfy Gorlas criteria.
213 - Ioana Cristescu 2011
We present a type system to guarantee termination of pi-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels. We show that our system imp roves over previously existing proposals by accepting more processes as terminating. This increased expressiveness allows us to capture sensible programming idioms. We demonstrate how our system can be extended to handle the encoding of the simply typed lambda-calculus, and discuss questions related to type inference.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا