CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

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 - 15:30: CPP - Session 7: Verification for Concurrent and Distributed Systems at Room St Petersburg II
CPP-2016-main14:00 - 14:30
Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
CPP-2016-main14: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 Washington
CPP-2016-main15:00 - 15:30
Michel St-MartinUniversity of Ottawa, Amy FeltyUniversity of Ottawa