This project aims to develop the foundations of an Isabelle/HOL library of process calculi, providing machine-checked syntax and operational semantics for a range of calculi alongside base definitions such as partial and complete traces and simple notions of semantic equivalence. The focus is breadth and reusability rather than deep meta-theory for a single calculus. Suitable as a 12- or 24-unit Honours or Masters project.
Background
Process algebras provide formal languages for describing and reasoning about concurrent and communicating systems. Dozens have been developed since the 1980s, ranging from the foundational calculi such as Milner’s CCS and Hoare’s CSP, to richer formalisms featuring data and broadcast communication such as mCRL2 and AWN. A notable mechanisation effort is Jesper Bengtson’s formalisation of the Psi-calculus in Isabelle/HOL on the Archive of Formal Proofs, which develops a deeply worked meta-theory for a single, expressive calculus. No comparable library currently provides a broad collection of process calculi formalised side-by-side with shared infrastructure.
Scope
The project will design a small core layer in Isabelle/HOL for representing process terms and structural operational semantics rules, and mechanise the syntax and semantics of at least two calculi of differing complexity—for example, CCS and a calculus featuring data or broadcast. On top of this, base definitions of partial and complete traces will be provided, together with a simple notion of semantic equivalence (e.g. trace equivalence) demonstrated on small examples. Emphasis is on clean abstractions, reusability, and a design that makes adding further calculi straightforward.
Expected Outcomes
The result will be a documented Isabelle/HOL library covering the syntax and operational semantics of several process calculi, with base definitions of traces and at least one notion of semantic equivalence, accompanied by worked examples. Ideally, the development is ready for submission to the Archive of Formal Proofs.
References
- J. Bengtson et al., Psi-calculi in Isabelle, Archive of Formal Proofs (https://isa-afp.org/search/?s=Psi%20calculus).
- R. Milner, Communication and Concurrency, Prentice Hall, 1989.
- C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985.
- J.F. Groote and M.R. Mousavi, Modeling and Analysis of Communicating Systems, MIT Press, 2014 (mCRL2).