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

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 2

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