Proof Theoretical Methods for Reasoning about Process Equivalence

Modern computation paradigms such as mobile and secure computing can be modelled formally in process calculi. These formal models can be used to analyse and to construct correct computer programs. Central to the analysis and construction of computer programs is the notion of process equivalence and the feasibility of mechanically checking this equivalence. Recent works in proof theoretical approach to process calculi have shown promising results in reasoning about equivalence for mobile processes. We will extend this approach to cover process calculi for secure computation, and provide the foundations for the mechanisation of equivalence checking.