Related papers: Contextual equivalence for higher-order pi-calculu…
The $\pi$-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how $\pi$-calculus processes can be controlled so that computations…
Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across subterms. In this approach, context splits redundantly echo…
We develop a version of the pi-calculus, picost, where channels are interpreted as resources which have costs associated with them. Code runs under the financial responsibility of owners; they must pay to use resources, but may profit by…
We present an extension of System F with higher-order context-free session types. The mixture of functional types with session types has proven to be a challenge for type equivalence formalization: whereas functional type equivalence is…
Gradual typing is an approach to integrating static and dynamic typing within the same language, and puts the programmer in control of which regions of code are type checked at compile-time and which are type checked at run-time. In this…
We consider the problem of symbolic reachability analysis of higher-order context-free processes. These models are generalizations of the context-free processes (also called BPA processes) where each process manipulates a data structure…
The Asynchronous pi-calculus, as recently proposed by Boudol and, independently, by Honda and Tokoro, is a subset of the pi-calculus which contains no explicit operators for choice and output-prefixing. The communication mechanism of this…
Locks are a classic data structure for concurrent programming. We introduce a type system to ensure that names of the asynchronous pi-calculus are used as locks. Our calculus also features a construct to deallocate a lock once we know that…
The $\pi$-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined…
The Asynchronous pi-calculus, proposed by Honda and Tokoro (1991) and, independently, by Boudol (1992), is a subset of the pi-calculus (Milner, 1992) which contains no explicit operators for choice and output-prefixing. The communication…
First, we extend Leifer-Milner RPO theory, by giving general conditions to obtain IPO labelled transition systems (and bisimilarities) with a reduced set of transitions, and possibly finitely branching. Moreover, we study the weak variant…
We introduce a novel approach to studying properties of processes in the {\pi}-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in…
Session types model structured communication-based programming. In particular, binary session types for the pi-calculus describe communication between exactly two participants in a distributed scenario. Adding sessions to the pi-calculus…
We introduce sound and complete labelled sequent calculi for the basic normal non-distributive modal logic L and some of its axiomatic extensions, where the labels are atomic formulas of the first order language of enriched formal contexts,…
The complexity of large-scale distributed systems, particularly when deployed in physical space, calls for new mechanisms to address composability and reusability of collective adaptive behaviour. Computational fields have been proposed as…
The theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are…
In any setting in which observable properties have a quantitative flavour, it is natural to compare computational objects by way of \emph{metrics} rather than equivalences or partial orders. This holds, in particular, for probabilistic…
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…
We present Hypersequent Classical Processes (HCP), a revised interpretation of the "Proofs as Processes" correspondence between linear logic and the {\pi}-calculus initially proposed by Abramsky [1994], and later developed by Bellin and…
We describe a process calculus featuring high level constructs for component-oriented programming in a distributed setting. We propose an extension of the higher-order pi-calculus intended to capture several important mechanisms related to…