pnp
所属分类：collect
开发工具：Coq
文件大小：0KB
下载次数：0
上传日期：2021-06-24 09:41:58
上 传 者：
sh-1993
说明： 关于通过SSReflect.在Coq中证明编程的短期课程的讲稿。，
(Lecture notes for a short course on proving programming in Coq via SSReflect.,)
文件列表:
LICENSE (1290, 2021-06-24)
Makefile (1489, 2021-06-24)
_CoqProject (586, 2021-06-24)
coq/ (0, 2021-06-24)
coq/BoolReflect.v (39164, 2021-06-24)
coq/Conclusion.v (5251, 2021-06-24)
coq/DepRecords.v (36710, 2021-06-24)
coq/FunProg.v (39452, 2021-06-24)
coq/HTT.v (103580, 2021-06-24)
coq/Introduction.v (22053, 2021-06-24)
coq/LogicPrimer.v (62838, 2021-06-24)
coq/Rewriting.v (34221, 2021-06-24)
coq/SsrStyle.v (41973, 2021-06-24)
docs/ (0, 2021-06-24)
docs/coq-logo.png (316695, 2021-06-24)
docs/hacking.html (2610, 2021-06-24)
docs/htt.zip (83297, 2021-06-24)
docs/index.html (4793, 2021-06-24)
docs/pnp.pdf (1366818, 2021-06-24)
docs/setup.html (7491, 2021-06-24)
docs/style.css (2317, 2021-06-24)
docs/test.v (304, 2021-06-24)
latex/ (0, 2021-06-24)
latex/coq-logo.png (316695, 2021-06-24)
latex/coqdoc.sty (5494, 2021-06-24)
latex/defs.tex (2025, 2021-06-24)
latex/mathpartir.sty (15251, 2021-06-24)
latex/pnp.tex (2276, 2021-06-24)
latex/proceedings.bib (13397, 2021-06-24)
latex/references.bib (19818, 2021-06-24)
lectures/ (0, 2021-06-24)
lectures/BoolReflect.v (20784, 2021-06-24)
lectures/DepRecords.v (12707, 2021-06-24)
lectures/FunProg.v (14040, 2021-06-24)
lectures/HTT.v (21802, 2021-06-24)
lectures/LogicPrimer.v (24456, 2021-06-24)
lectures/Rewriting.v (20378, 2021-06-24)
lectures/SsrStyle.v (26488, 2021-06-24)
... ...
# Programs and Proofs
[](https://doi.org/10.5281/zenodo.4996239)
A Short Course on Interactive Proofs in Coq/Ssreflect. This project
contains the Coq sources, the lectures and the exercises for the
course
**"Programs and Proofs: Mechanizing Mathematics with Dependent Types"**.
The latest draft of the accompanying lecture notes can be downloaded
from the official course page:
http://ilyasergey.net/pnp
Initial release: August 2014
## Building the Project
### Requirements
* [Coq](https://coq.inria.fr/download) (>= "8.10.0" & < "8.12~")
* [Mathematical Components](http://math-comp.github.io/math-comp/) `ssreflect` (>= "1.10.0" & < "1.12~")
* [FCSL-PCM](https://github.com/imdea-software/fcsl-pcm) (>= "1.0.0" & < "1.3~")
* [Hoare Type Theory](https://github.com/TyGuS/htt)
### Building
We recommend installing the requirements via [opam](https://opam.ocaml.org/doc/Install.html):
```
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add coq-htt git+https://github.com/TyGuS/htt\#master --no-action --yes
opam install coq coq-mathcomp-ssreflect coq-fcsl-pcm coq-htt
```
Then, run `make clean; make` from the root folder. This will compile
all lecture files, solutions and create the file `latex/pnp.pdf` with
lecture notes.
近期下载者：
相关文件：
收藏者：