Certifying confluence in a timed process calculus
Authors: Mehdi Dogguy and Stéphane Glondu.
We describe a type system for confluent processes using affine usages in a new timed variant of the π-calculus called Tapis. In any environment, typable programs are guaranteed to have the same behaviour. The operational semantics of the calculus and the proof of correctness of the type system are formalised and proved in Coq.
Licence: CeCILL
(which is GPL compatible)
Download: 1.0~rc1
(or browse files online).