All Projects → coq-community → coq-art

coq-community / coq-art

Licence: MIT license
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

Programming Languages

Coq
218 projects
HTML
75241 projects

Projects that are alternatives of or similar to coq-art

hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Stars: ✭ 38 (-33.33%)
Mutual labels:  coq, docker-coq-action
chapar
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Stars: ✭ 29 (-49.12%)
Mutual labels:  coq, docker-coq-action
gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Stars: ✭ 15 (-73.68%)
Mutual labels:  coq, docker-coq-action
bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
Stars: ✭ 20 (-64.91%)
Mutual labels:  coq, docker-coq-action
odd-order
The formal proof of the Odd Order Theorem
Stars: ✭ 20 (-64.91%)
Mutual labels:  coq
fcsl-pcm
Partial Commutative Monoids
Stars: ✭ 20 (-64.91%)
Mutual labels:  coq
go-learning
My Golang training material for testing smaller Go concepts and ideas.
Stars: ✭ 27 (-52.63%)
Mutual labels:  exercises
vericert
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Stars: ✭ 63 (+10.53%)
Mutual labels:  coq
FreeSpec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 48 (-15.79%)
Mutual labels:  coq
coq jupyter
Jupyter kernel for Coq
Stars: ✭ 70 (+22.81%)
Mutual labels:  coq
mcoq
Mutation analysis tool for Coq verification projects
Stars: ✭ 22 (-61.4%)
Mutual labels:  coq
streams-workshop
A workshop on Node.js Streams
Stars: ✭ 176 (+208.77%)
Mutual labels:  exercises
RiscvSpecFormal
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Stars: ✭ 69 (+21.05%)
Mutual labels:  coq
system-design-notebook
Learn System Design step by step
Stars: ✭ 372 (+552.63%)
Mutual labels:  exercises
studygroup
Repo containing exercises to learn Elixir
Stars: ✭ 14 (-75.44%)
Mutual labels:  exercises
react exercises
Exercises for Rithm School's free online React Fundamentals course
Stars: ✭ 28 (-50.88%)
Mutual labels:  exercises
Curso-Python-Gustavo-Guanabara
Mais de 100 exercícios resolvidos do curso de fundamentos de Python 3, ministrado pelo prof. Gustavo Guanabara do Curso em Vídeo.
Stars: ✭ 170 (+198.25%)
Mutual labels:  exercises
regex-reexamined-coq
No description or website provided.
Stars: ✭ 14 (-75.44%)
Mutual labels:  coq
fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Stars: ✭ 19 (-66.67%)
Mutual labels:  coq
rupicola
Gallina to Bedrock2 compilation toolkit
Stars: ✭ 41 (-28.07%)
Mutual labels:  coq

Coq'Art

Docker CI Contributing Code of Conduct Zulip DOI

Coq'Art is the familiar name for the first book on the Coq proof assistant and its underlying theory, the Calculus of Inductive Constructions. This project contains the Coq sources of all examples and the solution to 170 out of over 200 exercises from the book.

Meta

Building instructions

git clone https://github.com/coq-community/coq-art
cd coq-art
make   # or make -j <number-of-cores-on-your-machine>

Documentation

For more information, see the book website and the publisher's website.

This repository is also used as the source for the following web site.

The repository is structured as follows.

Book chapters

  1. A Brief Presentation of Coq
  2. Gallina: Coq as a Programming Language
  3. Propositions and Proofs
  4. Dependent Product
  5. Everyday Logic
  6. Inductive Data Structures
  7. Tactics and automation
  8. Inductive Predicates
  9. Functions and their specification
  10. Extraction and imperative programming
  11. A Case Study: binary search trees
  12. The Module System
  13. Infinite Objects and Proofs
  14. Foundations of Inductive Types
  15. General Recursion
  16. Proof by reflection

Additional material

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].