Search

• < Previous
• 1
• Next >

---

Cartesian closed 2-categories and permutation equivalence in higher-order rewriting

Tom Hirschowitz.

We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete.

---

Full abstraction for fair testing in CCS (expanded version)

Tom Hirschowitz.

In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent form of presheaf semantics and as a concurrent form of game semantics. We define in this setting an analogue of fair testing equivalence, which we prove fully abstract w.r.t. standard fair testing&nbsp;[&hellip;]

---

An intensionally fully-abstract sheaf model for $\pi$ (expanded version)

Clovis Eberhart ; Tom Hirschowitz ; Thomas Seiller.

Following previous work on CCS, we propose a compositional model for the $\pi$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair&nbsp;[&hellip;]

---

Modules over monads and operational semantics (expanded version)

André Hirschowitz ; Tom Hirschowitz ; Ambroise Lafont.

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as&nbsp;[&hellip;]

---

A categorical framework for congruence of applicative bisimilarity in higher-order languages

Tom Hirschowitz ; Ambroise Lafont.

Applicative bisimilarity is a coinductive characterisation of observational equivalence in call-by-name lambda-calculus, introduced by Abramsky (1990). Howe (1996) gave a direct proof that it is a congruence, and generalised the result to all languages complying with a suitable format. We propose a&nbsp;[&hellip;]

---

Variable binding and substitution for (nameless) dummies

André Hirschowitz ; Tom Hirschowitz ; Ambroise Lafont ; Marco Maggesi.

By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi's approach, with which we establish a strong&nbsp;[&hellip;]

---