WHAT I have done on the road to Coq language and certified programming.
-
tsinghua-coq-summer-school
Code for exercises of Tsinghua Coq Summer School by Yves Bertot and Pierre Castéran.
See more details at: https://www.labri.fr/perso/casteran/CoqArt/Tsinghua/index.html.
-
coq-art
Code for Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions by Yves Bertot and Pierre Castéran.
Coq'Art Home page: https://www.labri.fr/perso/casteran/CoqArt/.
-
cpdt
Code for Certified Programming with Dependent Types by Adam Chlipala.
Book's home page: http://adam.chlipala.net/cpdt/.
-
software-foundations
Code for Software Foundations by Benjamin C. Pierce.
Online version of Software Foundations: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html.
Open sourced under The MIT License. Copyright (c) 2015-2016 He Tao.