文件名称：NuprlInCoq:Nuprl类型理论在Coq中的实现
文件大小：2.53MB
文件格式：ZIP
更新时间：2024-06-12 07:59:06
Coq
制作文件 要生成Makefile，请运行create_makefile.sh 。 该脚本需要bash v4。 它将为rules.v及其依赖项生成一个Makefile。 每次拉动以更新Makefile时，请重新运行create_makefile.sh ，以防新文件已提交或文件已四处移动。 然后运行“ make”（或者，如果您的计算机具有多个内核，则运行make -jn，其中n是要使用的内核数）来编译所有内容。 这需要一段时间。 我们的实现使用Coq版本8.9.1（您可以通过opam获得）进行编译。 描述 该库自2016年以来正式化了Nuprl的构造类型理论（CTT）。可以在上找到有关Nuprl的更多信息。 （还可以检查以实现的SML重新实现。）至于 ， 和 ，Nuprl实现了从属类型理论àMartin-Löf。 但是，CTT是一种可扩展类型理论，最初是受Martin-Löf的可扩展类型理