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
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

14:00 - 15:30: Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II
14:00 - 14:30
Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
14:30 - 15:00
Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of Washington
15:00 - 15:30
Michel St-MartinUniversity of Ottawa, Amy FeltyUniversity of Ottawa