Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine- checked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework.
Bisimulation up-to techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psi- calculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up to-techniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.
Tue 19 Jan
|14:00 - 14:30|
|14:30 - 15:00|
Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of WashingtonPre-print
|15:00 - 15:30|