NuprlInCoq:Nuprl类型理论在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的可扩展类型理
文件下载
资源详情
[{"title":"（ 524 个子文件 2.53MB ） NuprlInCoq:Nuprl类型理论在Coq中的实现-源码","children":[{"title":"_CoqProject <span style='color:#111;'> 198B </span>","children":null,"spread":false},{"title":"univ_tacs.v <span style='color:#111;'> 13.43KB </span>","children":null,"spread":false},{"title":"sequents_lib.v <span style='color:#111;'> 9.55KB </span>","children":null,"spread":false},{"title":"per_props_uni.v <span style='color:#111;'> 8.21KB </span>","children":null,"spread":false},{"title":"seq_util2.v <span style='color:#111;'> 14.86KB </span>","children":null,"spread":false},{"title":"......","children":null,"spread":false},{"title":"<span style='color:steelblue;'>文件过多，未全部展示</span>","children":null,"spread":false}],"spread":true}]
评论信息
其他资源
- 三次样条函数计算（很完整看了就明白）
- 使用CLRC663芯片基于15693协议的读写
- 基于粒子群算法的机组组合计算
- 单片机简易计算器（包含设计报告，源程序及仿真）
- UWB matlab程序
- MVC三层+Dapper+分页
- 仿Chrome 风格的TabControl控件
- 北京大学语料库（1 833 177 字）包含训练和测试集
- 通过SD卡升级STM32F103程序
- 指纹生成工具SFingerDemo
- Editorial: Welcome to
- q_and_kdb+.pdf
- 根据excel中的数据生成多个word文件python程序
- C语言写的EGE图像库的推箱子源码.rar
- ChipEasy芯片无忧 V1.6 Beta3(U盘芯片检测工具,SSD,U盘主控)
- 智慧农场小程序V1.1.4
- ShoeStore穿美在线鞋城
- indy10.1.5_d7（delphi7上的indy）
- 显示农历属相(VB6.0代码)
免责申明
【只为小站】的资源来自网友分享，仅供学习研究，请务必在下载后24小时内给予删除，不得用于其他任何用途，否则后果自负。基于互联网的特殊性，【只为小站】 无法对用户传输的作品、信息、内容的权属或合法性、合规性、真实性、科学性、完整权、有效性等进行实质审查；无论 【只为小站】 经营者是否已进行审查，用户均应自行承担因其传输的作品、信息、内容而可能或已经产生的侵权或权属纠纷等法律责任。
本站所有资源不代表本站的观点或立场，基于网友分享，根据中国法律《信息网络传播权保护条例》第二十二条之规定，若资源存在侵权或相关问题请联系本站客服人员，zhiweidada#qq.com，请把#换成@，本站将给予最大的支持与配合，做到及时反馈和处理。关于更多版权及免责申明参见 版权及免责申明
本站所有资源不代表本站的观点或立场，基于网友分享，根据中国法律《信息网络传播权保护条例》第二十二条之规定，若资源存在侵权或相关问题请联系本站客服人员，zhiweidada#qq.com，请把#换成@，本站将给予最大的支持与配合，做到及时反馈和处理。关于更多版权及免责申明参见 版权及免责申明