Search

• < Previous
• 1
• Next >

---

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 semistructured data. We study some basic questions concerning the discriminating power of AL, focusing on the equivalence on&nbsp;[&hellip;]

---

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 data. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in&nbsp;[&hellip;]

---

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., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible&nbsp;[&hellip;]

---

Trees from Functions as Processes

Davide Sangiorgi ; Xian Xu.

Levy-Longo Trees and Bohm Trees are the best known tree structures on the {\lambda}-calculus. We give general conditions under which an encoding of the {\lambda}-calculus into the {\pi}-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the&nbsp;[&hellip;]

---

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 semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a&nbsp;[&hellip;]

---