proof-system - 有没有人使用证明助手来证明类型化过程演算的可靠性？

Question

......他们是否在我有能力阅读的地方发布了结果？

Answer 1

有几个人在做这些事情。查看 John Rushbie 的PVS站点上的论文，并查看Coq 的论文。

搜索Citeseer也可能有一些好处——现在几乎每个人都在 Citeseer 上发布他们的预印本，所以环顾四周通常会找到相同的论文，或者与昂贵期刊上发表的论文非常相似的东西。

Answer 2

啊，在 David N.Turner 的论文中，Pict 编程语言背后的过程演算的可靠性得到了证明。

Answer 3

形式证明档案在其主题中列出的“过程演算”类别中有几个条目，例如 CCS 和 Pi 演算。