Search

• < Previous
• 1
• Next >

---

Acyclic Solos and Differential Interaction Nets

Thomas Ehrhard ; Olivier Laurent.

We present a restriction of the solos calculus which is stable under reduction and expressive enough to contain an encoding of the pi-calculus. As a consequence, it is shown that equalizing names that are already equal is not required by the encoding of the pi-calculus. In particular, the induced&nbsp;[&hellip;]

---

Game semantics for first-order logic

Olivier Laurent.

We refine HO/N game semantics with an additional notion of pointer (mu-pointers) and extend it to first-order classical logic with completeness results. We use a Church style extension of Parigot's lambda-mu-calculus to represent proofs of first-order classical logic. We present some relations with&nbsp;[&hellip;]

---

Focusing in Orthologic

Olivier Laurent.

We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to add&nbsp;[&hellip;]

---