pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Index to example source files for chapters

Browse source
This commit is contained in:
Adam Chlipala 2016-02-13 19:45:22 -05:00
parent a0487bc153
commit 9ae318190c
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
README.md
View file

@ -3,3 +3,8 @@
This is an in-progress, open-source book by [Adam Chlipala](http://adam.chlipala.net/) simultaneously introducing [the Coq proof assistant](http://coq.inria.fr/) and techniques for proving correctness of programs. That is, the game is doing completely rigorous, machine-checked mathematical proofs, showing that programs meet their specifications. This is an in-progress, open-source book by [Adam Chlipala](http://adam.chlipala.net/) simultaneously introducing [the Coq proof assistant](http://coq.inria.fr/) and techniques for proving correctness of programs. That is, the game is doing completely rigorous, machine-checked mathematical proofs, showing that programs meet their specifications.
Just run `make` here to build everything, including the book `frap.pdf` and the accompanying Coq source modules. Just run `make` here to build everything, including the book `frap.pdf` and the accompanying Coq source modules.
# Code associated with the different chapters
* Chapter 2: `BasicSyntax.v`
* Chapter 3: `Interpreters.v`