Introduction to Coq - Part 1 of 2
summary
Hands-on walkthrough of Coq that actually builds proofs: uses intro/apply/assumption tactics plus elimination, cut, exact and unfold; loads examples from a GitHub repo and runs them in the Coq IDE and GitHub exercises. Proves simple propositions and lambda combinators (identity K and S, Y mentioned), shows how tactics transform goals step by step, and runs short exercises interactively so the proofs finish and evaluate in the IDE.
AI-written summary · about
chapters (16)
- 0:00Intro
- 1:58Welcome
- 3:09What is Coq
- 4:45What does Coq do
- 6:29Making proofs
- 9:26Introductions
- 15:12Other Taxes
- 17:06Other Things
- 18:01Classical Logic
- 19:19Coq IDE
- 21:00Proof
- 30:13Navigation
- 35:36References
- 37:21Labels
- 39:41Advice
- 43:31J Claremont
related talks
26mInteractive Theorem Provers for Proof Education
54mTheorem Proving in Coq using Tactics
38mAutomatically Synthesising Programs that We Can Trust
01h 44mAn Introduction to Natural Deduction
01h 46mWrite Some Idris
04mInterview
01h 16mCoding Agents: New opportunities for formal methods?
35mProof Theory Impressionism: Blurring the Curry-Howard Line