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.
发布评论
评论（3）
有几个人正在按照这些思路做事。 浏览 John Rushbie 的 PVS 网站上的论文，然后查看 Coq 的 论文。
搜索 Citeseer 可能也会有一些好处 - 现在几乎每个人都会在 Citeseer 上发布他们的预印本，所以有点环顾四周通常会得到同样的论文，或者与昂贵期刊上发表的论文非常相似的论文。
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.
啊，David N.Turner 的论文中证明了 Pict 编程语言底层的过程演算的合理性。
Ah, there is a proof of soundness for the process calculus underlying the Pict programming language in David N.Turner's thesis.
形式证明档案在其 主题，例如 CCS 和 Pi 微积分。
The Archive of Formal Proofs has several entries in the category "Process Calculi" listed in its topics, such as CCS and Pi Calculus.