Proving Theorems and Certifying Programs with Coq
summary
Concrete claims and code: Coq proofs are Gallina terms checked by the typechecker, Ltac scripts generate those terms, and proofs erase to runnable OCaml/Haskell via extraction; examples include dependent types (length-indexed lists), a verified concat implementation, and structural recursion that enforces termination. The demo shows using Gallina and Ltac to build proofs, viewing generated proof terms, using CoqIDE/ProofGeneral, and putting everything on the GitHub slides so the code and tactics can be inspected and re-run.
AI-written summary · about
chapters (25)
- 0:00Welcome to Coq
- 1:15Mathematical proofs and verification
- 3:22Programming and types
- 5:54Curry-Howard explained
- 8:03What is a theorem prover
- 10:30Coq setup and interfaces
- 11:56Basic types in Coq
- 14:11Inductive types for numbers
- 16:20Coq’s three languages
- 17:49Vernacular commands and IDE
- 18:10Simple functions in Coq
- 19:11Recursive functions and termination
- 21:20Dependent types intro
- 23:57Dependent lists by length
- 24:40Functions on dependent types
- 28:43Dependent pattern matching
- 31:40Logic and propositions
- 33:28Defining logical AND
- 39:58Coq foundations
- 41:01Proving true in Coq
- 46:37Proof mode and tactics
- 48:01First proof with tactics
- 51:10Tacticals and automation
- 53:24Proof scripts behind the scenes
- 54:10Other logical operators
related talks
26mData-Driven Lemma Synthesis for Interactive Proofs
22mTowards Verified Linear Algebra Programs Through Equivalence
06mLightning Talk: Curry-Howard Correspondence
19mTowards Mining Robust Coq Proof Patterns
52mKeynote: Tools for Verified Scala
43mPropositions as Types
01h 20mA Practical Introduction to Haskell GADTs
45m(Programming Languages) in Agda = Programming (Languages in Agda)