田春冰河
2019-09-02 00:00:00 发布
[2/3] 我今天一鼓作气，终于彻底完成了 CCS 进一步形式化工作（本质上就只有两个新定理），因为后期出了错误不得不回炉好几个引理的证明，比预计的进度晚了两天。核心代码 4000 多行，还优化了的一些旧定理的证明，所有代码作为一个巨大的 PR 刚刚已经发给 HOL 官方了。网页链接