Let Curry-Howard code for me
summary
Shows a concrete proof of the Curry-Howard correspondence by building and extracting code for Euclidean division by two, using dependent types to encode the relation between input n and quotient y and proving it in Coq. The script uses induction/GTW style recursion, dissects base and n+2 cases, constructs witnesses, and runs Coq’s program extraction to produce executable code, noting that extraction sometimes emits awkward but correct routines.
AI-written summary · about
chapters (12)
- 0:00Curry-Howard correspondence
- 1:56Division with dependent types
- 6:59Simple to Euclidean division
- 8:06Coq proof assistant
- 10:18Proofs for division by two
- 13:30Induction in Coq proofs
- 16:00Division cases zero and one
- 17:30Inductive step n minus two
- 18:34Proof summary and extraction
- 20:00Theorem to executable code
- 21:26Curry-Howard applications
- 22:03Q&A
related talks
01h 12mTruth about Types
56mWrite You Some Proofs for Great Good
43mLearning Computer Architecture
55mKeynote: Propositions as Types
55mHands on With Recursion Schemes - Part 2 of 2
01h 02mDiscovering a User-Facing Concept
31mParametricity The Essence of Information Hiding
34mCommunication, Expression, and Types: Your Compiler as an Ally