Search

• < Previous
• 1
• Next >

---

Modal Logics for Nominal Transition Systems

Joachim Parrow ; Johannes Borgström ; Lars-Henrik Eriksson ; Ramūnas Forsberg Gutkovas ; Tjark Weber.

We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and&nbsp;[&hellip;]

---

A Sorted Semantic Framework for Applied Process Calculi

Johannes Borgström ; Ramūnas Gutkovas ; Joachim Parrow ; Björn Victor ; Johannes Åman Pohjola.

Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are&nbsp;[&hellip;]

---

The Largest Respectful Function

Joachim Parrow ; Tjark Weber.

Respectful functions were introduced by Sangiorgi as a compositional tool to formulate short and clear bisimulation proofs. Usually, the larger the respectful function, the easier the bisimulation proof. In particular the largest respectful function, defined as the pointwise union of all respectful&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;]

---

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;]

---