#lang

Reduction, a pervasive idea in computer science, is often taught in algorithm courses with NP problems. The traditional pen-and-paper approach is notoriously ineffective both for students and instructors: Subtle mistakes in reductions are often hard to detect by merely inspecting the purported solutions. Constructing a counterexample by hand to expose the mistake is even more onerous. Based on the observation that reductions are actually programs, we designed #lang Karp, a DSL for formulating and random testing NP reductions. In this talk, I’m going to discuss the implementation of Karp on top of Racket and solver-aided host language Rosette.
con.racket-lang.org