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

Question

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

Answer 1

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

Answer 2

There are several people doing things along those lines. Look through the papers at John Rushbie's PVS site, and look at Coq's papers.

Searching Citeseer will probably do some good too — almost everyone nowadays publishes their preprints to Citeseer, so a little looking around will usually get you the same paper, or something very very similar to the paper published in the expensive journal.

Answer 3

The Archive of Formal Proofs has several entries in the category "Process Calculi" listed in its topics, such as CCS and Pi Calculus.