Thu 16 Jun 2022 14:30 - 14:50 at Toucan - Numbers Chair(s): Chandrakana Nandi
Fri 17 Jun 2022 02:30 - 02:50 at Toucan - Numbers

In CS theory courses, proofs by reduction 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, reductions are subtle yet, most of the time, unimplemented programs. And for a good reason: there exists no language tailored to reductions.

We introduce Karp, a language for programming and testing Karp 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 from a preliminary user study with Karp.

Thu 16 Jun

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:50
NumbersPLDI at Toucan +12h
Chair(s): Chandrakana Nandi Certora, inc.
13:30
20m
Talk
Choosing Mathematical Function Implementations for Speed and Accuracy
PLDI
Ian Briggs University of Utah, Pavel Panchekha University of Utah
DOI
13:50
20m
Talk
Guaranteed bounds for posterior inference in universal probabilistic programming
PLDI
Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford, Fabian Zaiser University of Oxford
DOI Pre-print
14:10
20m
Talk
Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries
PLDI
Mridul Aanjaneya Rutgers University, Jay P. Lim Yale University, Santosh Nagarakatte Rutgers University
Link to publication DOI Pre-print
14:30
20m
Talk
Karp: A Language for NP Reductions
PLDI
Chenhao Zhang Northwestern University, Jason D. Hartline Northwestern University, Christos Dimoulas PLT @ Northwestern University
DOI

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

01:30 - 02:50
NumbersPLDI at Toucan
01:30
20m
Talk
Choosing Mathematical Function Implementations for Speed and Accuracy
PLDI
Ian Briggs University of Utah, Pavel Panchekha University of Utah
DOI
01:50
20m
Talk
Guaranteed bounds for posterior inference in universal probabilistic programming
PLDI
Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford, Fabian Zaiser University of Oxford
DOI Pre-print
02:10
20m
Talk
Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries
PLDI
Mridul Aanjaneya Rutgers University, Jay P. Lim Yale University, Santosh Nagarakatte Rutgers University
Link to publication DOI Pre-print
02:30
20m
Talk
Karp: A Language for NP Reductions
PLDI
Chenhao Zhang Northwestern University, Jason D. Hartline Northwestern University, Christos Dimoulas PLT @ Northwestern University
DOI