Coq的基础

Question

我假设Coq会在某一时刻转向LCF方法。在过去，我对foundations of the kernel in Isabelle感到好奇。我在一篇总结了现有文献的硕士论文中找到了对Isabelle/Pure的一些很好的描述。

我想知道是否有关于Coq内核的描述，涵盖了它的逻辑和实现方面。

Answer 1

我认为你的问题和How does one implement Coq?很相似。至少我想给出一个类似的答案。

我认为MetaCoq是指定和(部分)验证Coq内核：https://github.com/MetaCoq/metacoq的最先进的成果。它最初是一个用于在Coq中进行元编程的库，因此实现了Coq中内核的表示。它已经发展了很多，现在包含了Coq (的一个子集)的类型规则，以及几个元理论属性的形式化，一个类型检查器和一个擦除机制。

现在理解你的问题：Coq reference manual已经提供了归纳构造演算的某种规范，它应该始终与最新版本的Coq保持同步。

MetaCoq Project论文还试图对累积归纳结构的谓词演算进行规范。您似乎认为，当在证明助手本身中完成时，这可能没有纸张规范那么有价值，显然我并不完全这样认为(但我是作者之一，我是有偏见的)。这是一个值得关注的问题，但至少就规范而言，它只会使其比在纸上完成的更精确。Coq参考手册有时可能不精确。我们的工作还迫使我们对ocaml中没有强制执行的表示的显式不变量。此外，我们将实现和规范分开( Coq参考手册非常面向实现)。可以说，在这种分离上还需要做更多的工作。

另外，通常人们处理这些演算的子集，特别是考虑到归纳类型，这是相当痛苦的完全布局。