Contents

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

There are some free resources for learning Coq, such as:

* Software Foundations series:
    + [Volume 1: Logical Foundations](https://softwarefoundations.cis.upenn.edu/lf-current/index.html)
    + [Volume 2: Programming Language Foundations](https://softwarefoundations.cis.upenn.edu/plf-current/index.html)
    + [Volume 3: Verified Functional Algorithms](https://softwarefoundations.cis.upenn.edu/vfa-current/index.html)
* Certified Programming with Dependent Types:
    + Which is avalaible for free in [Adam Chipala's site](http://adam.chlipala.net/cpdt/).

Version data entries

39 entries across 39 versions & 1 rubygems

Version	Path
trackler-2.2.1.180	tracks/coq/docs/LEARNING.md
trackler-2.2.1.179	tracks/coq/docs/LEARNING.md
trackler-2.2.1.178	tracks/coq/docs/LEARNING.md
trackler-2.2.1.177	tracks/coq/docs/LEARNING.md
trackler-2.2.1.176	tracks/coq/docs/LEARNING.md
trackler-2.2.1.175	tracks/coq/docs/LEARNING.md
trackler-2.2.1.174	tracks/coq/docs/LEARNING.md
trackler-2.2.1.173	tracks/coq/docs/LEARNING.md
trackler-2.2.1.172	tracks/coq/docs/LEARNING.md
trackler-2.2.1.171	tracks/coq/docs/LEARNING.md
trackler-2.2.1.170	tracks/coq/docs/LEARNING.md
trackler-2.2.1.169	tracks/coq/docs/LEARNING.md
trackler-2.2.1.167	tracks/coq/docs/LEARNING.md
trackler-2.2.1.166	tracks/coq/docs/LEARNING.md
trackler-2.2.1.165	tracks/coq/docs/LEARNING.md
trackler-2.2.1.164	tracks/coq/docs/LEARNING.md
trackler-2.2.1.163	tracks/coq/docs/LEARNING.md
trackler-2.2.1.162	tracks/coq/docs/LEARNING.md
trackler-2.2.1.161	tracks/coq/docs/LEARNING.md
trackler-2.2.1.160	tracks/coq/docs/LEARNING.md