This article is indeed very interesting. I've read somewhere that there's a more recent, extended version of it available via the ACM Digital Library. For cor

This article is indeed very interesting. I've read somewhere that there's a more recent, extended version of it available via the ACM Digital Library. For correctness proving, you may look for example in http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.101.4119&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.101... . It is constrained to π-calculus though.