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

• Fall 2023 - Boston University
• Fall 2022 - Sabancı University

Other resources

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

• The Software Foundations suite
• The Mathematical Components Book
• Programs and Proofs by Ilya Sergey
• Certified Programming with Dependent Types and Formal Reasoning About Programs
• The Coq’Art book