Milawa on Jitawa：经过验证的定理证明者 | Lambda the Ultimate Lambda the Ultimate 主页 反馈 常见问题解答 入门讨论 网站运营讨论 最近的帖子（新主题） 部门 课程 研究论文 设计文档 引文 谱系图 档案 用户登录 创建新帐户 请求新密码 导航最近的帖子 Home Milawa on Jitawa: 经过验证的定理证明者 Milawa 2010 年 8 月 – 2011 年 5 月。
Magnus Myreen 开发了一个经过验证的 Lisp 系统，名为 Jitawa，它可以运行 Milawa。
我们关于这个项目的论文被 ITP 2011 接受。
这非常有趣：Milawa 已经在“自我验证”，正如页面上解释的那样。
最近，它被设计为在经过验证的 Lisp 运行时上运行，这意味着直到 X86_64 机器代码的整个堆栈都经过验证。
由于 HOL4 是一个“类似 LCF”的系统，因此只要您信任 LCF 流程，您就可以做到这一点，但它不像 Milawa 或 Coq 那样满足 de Bruijn 标准。
来源：HackerNews New
