Free Books on the Coq Language & Proof Assistant
People are talking about using formal methods and more specifically formal proofs in the context of the blockchain. I just provide a few pointers for Coq: the recent developments and efforts are interesting and worth following:
- A formally verified compiler for C which is Xavier Leroy's project for several years now: http://compcert.inria.fr/ . It is a huge project with a ton of work.
- Bedrock is interesting too, it is a library of building blocks to manipulate for instance pointers, data and specifications: http://plv.csail.mit.edu/bedrock/.
- Package lists: https://coq.inria.fr/opam/www/
- It is a live and active community.
Still, in my humble opinion it is not something that is easy to understand, or to perform, even if you already have a good idea of the formal proof.
Tutorials:
- Mike Nahas: https://coq.inria.fr/tutorial-nahas
- Pierre Castéran & several authors: http://www.labri.fr/perso/casteran/index.html
Classes:
- Yves Bertot and Pierre Castéran: http://www.labri.fr/perso/casteran/CoqArt/Tsinghua/index.html
- Check Adam Chlipala book page, where there is a list of classes at the end: http://adam.chlipala.net/cpdt/
List of Books:
Coq'Art by Yves Bertot and Pierre Castéran, only the french edition is freely available (http://www.springer.com/gp/book/9783540208549)
Certified Programming with Dependent Types by Adam Chlipala: http://adam.chlipala.net/cpdt/
Software Foundations Series: https://softwarefoundations.cis.upenn.edu/ which is a recent effort on Coq and covers many other subjects: semantics, models for instance:
- Logical Foundations: https://softwarefoundations.cis.upenn.edu/lf-current/index.html
- Programming Language Foundations: https://softwarefoundations.cis.upenn.edu/plf-current/index.html
- Verified Functional Algorithms : https://softwarefoundations.cis.upenn.edu/vfa-current/index.html
Good post my friend...thanks for sharing.
I like your post @boucaron
Thank you
This post received a 3.64% upvote from @randowhale thanks to @boucaron! To learn more, check out @randowhale 101 - Everything You Need to Know!
Congratulations @boucaron! You have completed some achievement on Steemit and have been rewarded with new badge(s) :
Click on any badge to view your own Board of Honor on SteemitBoard.
For more information about SteemitBoard, click here
If you no longer want to receive notifications, reply to this comment with the word
STOPThis post has received a 34.48 % upvote from
thanks to: @boucaron.
For more information, click here!
@boucaron take part of the @minnowhelper's 50 SBD Contest. For more information, click here!
img credz: pixabay.com
Nice, you got a 2.2% @minnowbooster upgoat, thanks to @boucaron
Want a boost? Minnowbooster's got your back!
The @OriginalWorks bot has determined this post by @boucaron to be original material and upvoted it!
To call @OriginalWorks, simply reply to any post with @originalworks or !originalworks in your message!
To enter this post into the daily RESTEEM contest, upvote this comment! The user with the most upvotes on their @OriginalWorks comment will win!
For more information, Click Here!
Special thanks to @reggaemuffin for being a supporter! Vote him as a witness to help make Steemit a better place!
This post has received a 1.20 % upvote from @booster thanks to: @boucaron.