TY - GEN
T1 - Karp
T2 - 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022
AU - Zhang, Chenhao
AU - Hartline, Jason D.
AU - Dimoulas, Christos
N1 - Publisher Copyright:
© 2022 ACM.
PY - 2022/6/9
Y1 - 2022/6/9
N2 - In CS theory courses, NP reductions are a notorious source of pain for students and instructors alike. Invariably, students use pen and paper to write down reductions that "work"in many but not all cases. When instructors observe that a student's reduction deviates from the expected one, they have to manually compute a counterexample that exposes the mistake. In other words, NP reductions are subtle yet, most of the time, unimplemented programs. And for a good reason: there exists no language tailored to NP reductions. We introduce Karp, a language for programming and testing NP reductions. Karp combines an array of programming languages techniques: language-oriented programming and macros, solver-aided languages, property testing, higher-order contracts and gradual typing. To validate the correctness of Karp, we prove that its core is well-defined. To validate its pragmatics, we demonstrate that it is expressive and performant enough to handle a diverse set of reduction exercises from a popular algorithms textbook. Finally, we report the results from a preliminary user study with Karp.
AB - In CS theory courses, NP reductions are a notorious source of pain for students and instructors alike. Invariably, students use pen and paper to write down reductions that "work"in many but not all cases. When instructors observe that a student's reduction deviates from the expected one, they have to manually compute a counterexample that exposes the mistake. In other words, NP reductions are subtle yet, most of the time, unimplemented programs. And for a good reason: there exists no language tailored to NP reductions. We introduce Karp, a language for programming and testing NP reductions. Karp combines an array of programming languages techniques: language-oriented programming and macros, solver-aided languages, property testing, higher-order contracts and gradual typing. To validate the correctness of Karp, we prove that its core is well-defined. To validate its pragmatics, we demonstrate that it is expressive and performant enough to handle a diverse set of reduction exercises from a popular algorithms textbook. Finally, we report the results from a preliminary user study with Karp.
KW - domain-specific language
KW - reduction
KW - solver-aided program- ming
KW - teaching and learning theoretical computer science
UR - http://www.scopus.com/inward/record.url?scp=85132264308&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85132264308&partnerID=8YFLogxK
U2 - 10.1145/3519939.3523732
DO - 10.1145/3519939.3523732
M3 - Conference contribution
AN - SCOPUS:85132264308
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 762
EP - 776
BT - PLDI 2022 - Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
A2 - Jhala, Ranjit
A2 - Dillig, Isil
PB - Association for Computing Machinery
Y2 - 13 June 2022 through 17 June 2022
ER -