# 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.

http://www.it.uu.se/research/upmarc/research/pl/applied-calculi