@inproceedings{'Mon4',
title = {{Formalisation of the Join-Calculus in Type Theory },
author = {Monin, Jean-Fran\c{c}ois},
month = {MAY},
year = {2004},
booktitle = {International Worshop on Formal Methods and Security}},
address = {Nankin},
team = {PACSS},
abstract = {Towards verifying mobile code, we choose to formalize an appropriate elementary model of concurrency in type theory (more precisely: the calculus of inductive constructions, CIC, implemented in the Coq proof assistant). The chosen process calculus is the Join-Calculus (JC) of Fournet, Gonthier and Levy. The latter can be seen as a variant of the pi-calculus of Milner, Parrow and Walker, with better locality properties. We use Coq for encoding a structural operational semantics of JC based on the reflexive chemical abstract machines model. Our formalisation uses the full power of inductive constructions and dependent types available in the underlying theory of Coq, in order to capture the reflexive features of JC.},
}
