Introduction to Coq - Part 2 of 2
summary
Continues a hands‑on Coq workshop that shows actual proofs, tactics and extracted code: step‑by‑step proofs use intro apply exact split induction on encoded naturals and lists, pattern matching and structural recursion to ensure termination, a worked predecessor and addition and a case proof of equality/existence. Demonstrates extraction to OCaml Haskell Scala from the proved definitions, notes the generated code works though performance is modest, and highlights where tactics like omega discriminate rewrite close goals.
AI-written summary · about
chapters (6)
- 0:00Start
- 29:49Lambda Calculus
- 32:57Structural Recursion
- 34:34Dependent Type
- 44:22Constructors
- 46:31Induction Principle
related talks
17mAnother Introduction to Cocotb
09mCollaborating with your computer using typed holes!
30mThrough the lens of Haskell: exploring new ideas for library design
29mBeyond Unit Tests: Taking Your Testing to the Next Level
23mHow cocotb made Python-powered verification mainstream -- and what comes next
31mPerformance Pitfalls: Tales From a Python/OCaml Codebase
02h 06mETA lang a Journey from Haskell via STG and Bytecode to Assembly Part 2
01mCodyssey: A playful control system workshop