Search

• < Previous
• 1
• Next >

---

Formalising the pi-calculus using nominal logic

Jesper Bengtson ; Joachim Parrow.

We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely&nbsp;[&hellip;]

---

Psi-calculi: a framework for mobile processes with nominal data and logic

Jesper Bengtson ; Magnus Johansson ; Joachim Parrow ; Björn Victor.

The framework of psi-calculi extends the pi-calculus with nominal datatypes for data structures and for logical assertions and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Psi-calculi can capture the same phenomena as&nbsp;[&hellip;]

---

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic

Jonas Kastberg Hinrichsen ; Jesper Bengtson ; Robbert Krebbers.

Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for&nbsp;[&hellip;]

---