My research focuses on process calculi and theorem proving. I am currently working with the mobility group on creating a generic environment for reasoning about process calculi in the interactive theorem prover Isabelle. To this end, I have modelled the pi-calculus in Isabelle using nominal logic. The proofs I have done so far are that strong equivalence is a congruence as well as all the structural congruence rules for strong bisimulation and strong equivalence. The Isabelle sources can be found here.

Formalising process calculi

I have finished writing my Ph.D. thesis. It can be downloaded from my thesis page, which also contains all Isabelle sources.

Hot off the presses

Psi-calculi: A framework for mobile processes with nominal data and logic Submitted 2009

I have formalised the results of both of these papers in the interactive theorem prover Isabelle. The sources can be found here. These theories have been developed using Mercurial version 96d053e00ec0 from the Isabelle repository. We are currently working on a version compatible with the latest release, in order to submit to the Isabelle Archive of Formal Proofs.

Publications