Personal tools
You are here: Home Events Johannes Borgström - Lab Lunch 2011

Johannes Borgström - Lab Lunch 2011

Psi-calculi: mobile processes from nominal data and logic

When modelling real world problems in pure process calculi one soon
discovers that the model becomes big and hard to understand due to a
lack of more complex datatypes and constructs. To address this,
several "applied" calculi have emerged, e.g. the spi-calculus and the
applied pi-calculus.

In an attempt to unify these extensions and to get simpler semantics
we are developing a framework in which applied calculi can be
formulated. Since the meta-theory of applied process calculi is
complicated and prone to errors, we formalize the theory in the
theorem prover Isabelle/HOL-Nominal as it is being developed, thereby
ensuring that the theory is indeed correct.

I will talk about the basic framework and sketch some recent
developments and lessons learned during the development.

This is work by the mobility group at Uppsala University, headed by
Joachim Parrow.

Document Actions