Title: “Real World Coq – An introduction to effective theorem proving”

Title: “Real World Coq – An introduction to effective theorem proving”

Real World Coq is an ongoing project to create an online interactive theorem proving course, aimed to complement existing teaching materials with more advanced theorem proving patterns seen in other courses.

As of today, we have done several short tutorials, the materials are available online.

Editions

Other resources

Real World Coq is designed to complement existing Coq teaching materials, a non-exhaustive list can be found below: