24 citations · 74 across the 13 of their papers we have counts for
13 papers
Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics
Guilheme Jaber, Davide Sangiorgi
We establish a tight connection between two models of the -calculus, namely Milner's encoding into the -calculus (precisely, the Internal -calculus), and operational game…
Extensional and Non-extensional Functions as Processes
Ken Sakayori, Davide Sangiorgi
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure -calculus, the process representations yield (at bes…
Eager Functions as Processes (long version)
Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi
We study Milner's encoding of the call-by-value -calculus into the -calculus. We show that, by tuning the encoding to two subcalculi of the -calculus (Internal and Asy…
Eager Functions as Processes
Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi
We study Milner's encoding of the call-by-value -calculus into the -calculus. We show that, by tuning the encoding to two subcalculi of the -calculus (Internal and Asy…
On sequentiality and well-bracketing in the -calculus
Daniel Hirschkoff, Enguerrand Prebet, Davide Sangiorgi
The -calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable be…
Modular coinduction up-to for higher-order languages via first-order transition systems
Jean-Marie Madiot, Damien Pous, Davide Sangiorgi
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., C…
Unique Solutions of Contractions, CCS, and their HOL Formalisation
Chun Tian, Davide Sangiorgi
The unique solution of contractions is a proof technique for bisimilarity that overcomes certain syntactic constraints of Milner's "unique solution of equations" technique. The pap…
Divergence and unique solution of equations
Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure sem…
Trees from Functions as Processes
Davide Sangiorgi, Xian Xu
Levy-Longo Trees and Bohm Trees are the best known tree structures on the λ-calculus. We give general conditions under which an encoding of the λ-calculus into the π-calculus is so…
On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version)
Ugo Dal Lago, Davide Sangiorgi, Michele Alberti
We study bisimulation and context equivalence in a probabilistic -calculus. The contributions of this paper are threefold. Firstly we show a technique for proving congruence of…
Light Logics and Higher-Order Processes
Ugo Dal Lago, Simone Martini, Davide Sangiorgi
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 pres…
Separability in the Ambient Logic
Daniel Hirschkoff, Etienne Lozes, Davide Sangiorgi
The \it{Ambient Logic} (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistruc…
On the Expressiveness of the Ambient Logic
Daniel Hirschkoff, Etienne Lozes, Davide Sangiorgi
The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured…