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... . It is constrained to π-calculus though.