Karp: A Language for NP Reductions
summary
Karp is a domain-specific language that encodes NP reductions as runnable programs, derives problem solvers by translating verifiers to Rosette for symbolic verification, and uses phase‑aware random generators for property-based testing. The paper encodes 26 textbook reductions, synthesizes instance generators, and catches injected bugs (10 buggy variants) with average test runs under two minutes each, showing practical expressiveness and bug-finding on standard classroom exercises.
AI-written summary · about
chapters (6)
- 0:00Start
- 3:42Recap of Mp Problems and Reductions
- 5:14Formal Definitions
- 12:11Random Testing
- 14:04Research Questions
- 21:02Polynomial Time Guarantee
related talks
51mSynthesis and Verification for All
15mProducts of Recursive Programs for Hypersafety Verification
31mProgramming Languages Must Have Formal Semantics. Period.
11mThe full-reducing Krivine abstract machine KN simulates pure normal-order reduction i...
15mClosing Remarks
31mA Coq Library of Undecidable Problems
20mKanren Light
34mLanguage Design Where Paradigms Meet