文件名称：lambdacplus:基于构造微积分的证明助手
文件大小：3.2MB
文件格式：ZIP
更新时间：2024-05-02 07:09:43
dependent-types theorem-proving proof-assistant type-theory JavaScript
λC+ 简短的一行描述 λC+是基于构造微积分（CoC）的证明助手。 到底是什么 λC+的核心是基于CoC的依赖类型的lambda演算的实现。 Curry-Howard对应关系使我们可以将逻辑连接词和量词编码为λC+中的类型。 这使我们可以将其视为校对助手。 眼镜 请参考latex目录。 网页界面 为了易于使用该语言，请下载位于主项目目录中的index.html和main.bc.js文件。 然后在您喜欢的浏览器中打开html文件。 由ACE编辑器提供支持的友好的基于Web的IDE将在这里与您打招呼。 样品证明 -- Formalization of Lawvere's fixed point theorem, which captures the essence of -- the diagonal argument as found in Cantor's famous theorem
【文件预览】：
lambdacplus-main
----bin()
--------dune(147B)
--------main.ml(3KB)
----mode-lambdacplus.js(2KB)
----package.json(798B)
----latex()
--------preamble.tex(4KB)
--------presentation.tex(14KB)
--------.gitignore(3KB)
--------spec.tex(83KB)
--------cs2104()
--------spec.pdf(241KB)
--------presentation.pdf(118KB)
----test()
--------dune(38B)
--------cs4215_dependent_types.ml(0B)
----run_main.sh(58B)
----dune-project(54B)
----sample_programs()
--------axiom_of_choice.lean(2KB)
--------disjunction.lean(684B)
--------wrong_type_ascription.txt(503B)
--------conjunction.lean(525B)
--------axiom_of_choice.txt(959B)
--------axiom_of_choice2.txt(2KB)
--------cantor.lean(3KB)
--------test_exists.lean(2KB)
--------cantor2.txt(3KB)
--------cantor.txt(2KB)
--------sample2.txt(198B)
--------sample_simple.txt(36B)
--------distributivity.lean(785B)
--------cantor2.lean(3KB)
--------sample1.txt(591B)
--------sample3.txt(103B)
----index.html(4KB)
----main.bc.js(11.5MB)
----.gitignore(348B)
----lambdacplus.opam(0B)
----lib()
--------error_reporting.mli(704B)
--------pretty_print.ml(3KB)
--------dune(118B)
--------error_reporting.ml(5KB)
--------parsing()
--------common()
--------pretty_print.mli(211B)
--------ast_conv.ml(11KB)
--------ast_conv.mli(1KB)
--------kernel()
----README.md(7KB)