Using the Design Recipe in Theory of Computation
summary
Adapts the Design Recipe from How to Design Programs to teach inductive proofs by deriving proof templates directly from recursive data definitions (regular expressions require six cases), uses those structural templates to place inductive hypotheses where the data recurses, avoids proof assistants and programming assignments, and reports modest improvement across several semesters though results remain imperfect; the concrete artifact is a reusable template method that consistently reduces common student errors.
AI-written summary · about
chapters (12)
- 0:00Proof by induction struggles
- 2:35Induction teaching flaws
- 6:03Textbook induction problems
- 10:44Terminology in computation
- 13:36Induction versus theory
- 15:22Induction as recursion
- 16:50Teaching recursion with data
- 20:02Design recipe for induction
- 23:41Why not use theorem provers
- 26:39Recursive data types solution
- 27:44Student progress results
- 28:25Q&A
related talks
35mHow to make ad hoc proof automation less ad hoc
25mRecursive Program Synthesis using Paramorphisms
01h 00mUnconference Coq
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
57mCrash Course on Notation in Programming Language Theory (Part 1)
01h 34mFormal Logic Undressed
20mTrace-Guided Inductive Synthesis of Recursive Functional Programs
01h 03mCrash Course on Notation in Programming Language Theory (Part 2)