Has anybody used a proof assistant to prove soundness of a typed process calculus?

...And have they published the results where I can afford to read them?

Ah, there is a proof of soundness for the process calculus underlying the Pict programming language in David N.Turner's thesis.