[[https://rocq-prover.org|Site web]]

=====Documentation=====

[[https://softwarefoundations.cis.upenn.edu/|Université de Pennsylvanie]] {{ :lang:rocq:1-logical_foundations-v6.9.0-9.0.tgz |Archive Logical Foundations v9.0.0}} {{ :lang:rocq:2-programming_language_foundations-v6.9.0-9.0.tgz |Programming Language Foundations v9.0.0}} {{ :lang:rocq:3-verified_functional_algorithms-v1.6.0-9.0.tgz |Verified Functional Algorithms v9.0.0}} {{ :lang:rocq:4-quickchick_-_property-based_testing_in_coq-v1.4.0-9.0.tgz |QuickChick: Property-Based Testing in Coq v9.0.0}} {{ :lang:rocq:5-verifiable_c-v1.2.2-8.16.tgz |Verifiable C v8.16}} {{ :lang:rocq:6-separation_logic_foundations-v2.4.0-9.0.tgz |Separation Logic Foundations v9.0.0}}

[[http://adam.chlipala.net/cpdt/|Adam Chlipala]] {{ :prive:lang:rocq:certified_programming_with_dependent_types_chlipala_a_.pdf |Archive}}

[[https://www.labri.fr/perso/casteran/CoqArt/|Coq'Art]] en français. {{ :lang:rocq:coqartf.pdf |Archive}}