This is an invited talk by Chenhao Zhang. Chenhao Zhang is a Ph.D. student in the CS Theory Group at Northwestern University, advised by Prof. Jason Hartline.

Abstract

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 Karp, a DSL for formulating and random testing NP reductions, combining multiple programming language techniques: language-oriented programming and macros, solver-aided languages, property testing, higher-order contracts, and gradual typing. In this talk, I will talk about the details of the encoding and abstraction of structures in Karp, particularly graphs, on top of the intermediate language Rosette as forms friendly to SMT solvers.