POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Wed 17 Jan 2024 10:30 - 10:50 at Kelvin Lecture - Synthesis 1 Chair(s): Soham Chakraborty

Achieving speed and accuracy for math library functions like exp, sin, and log is difficult. This is because low-level implementation languages like C do not help math library developers catch mathematical errors, build implementations incrementally, or separate high-level and low-level decision making. This ultimately puts development of such functions out of reach for all but the most experienced experts. To address this, we introduce MegaLibm, a domain-specific language for implementing, testing, and tuning math library implementations. MegaLibm is safe, modular, and tunable. Implementations in MegaLibm can automatically detect mathematical mistakes like sign flips via semantic well-formedness checks, and components like range reductions can be implemented in a modular, composable way, simplifying implementations. Once the high-level algorithm is done, tuning parameters like working precisions and evaluation schemes can be adjusted through orthogonal tuning parameters to achieve the desired speed and accuracy. MegaLibm also enables math library developers to work interactively, compiling, testing, and tuning their implementations and invoking tools like Sollya and type-directed synthesis to complete components and synthesize entire implementations. MegaLibm can express 8 state-of-the-art math library implementations with comparable speed and accuracy to the original C code, and can synthesize 5 variations and 3 from-scratch implementations with minimal guidance.

Wed 17 Jan

Displayed time zone: London change

10:30 - 11:50
Synthesis 1POPL at Kelvin Lecture
Chair(s): Soham Chakraborty TU Delft
10:30
20m
Talk
Implementation and Synthesis of Math Library FunctionsDistinguished Paper
POPL
Ian Briggs University of Utah, Yash Lad University of Utah, Pavel Panchekha University of Utah
10:50
20m
Talk
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
POPL
Yuantian Ding Purdue University, Xiaokang Qiu Purdue University
11:10
20m
Talk
Efficient Bottom-Up Synthesis for Programs with Local Variables
POPL
Xiang Li University of Michigan, Ann Arbor, Xiangyu Zhou University of Michigan, Rui Dong University of Michigan, Yihong Zhang University of Washington, Xinyu Wang University of Michigan
Pre-print
11:30
20m
Talk
Optimal Program Synthesis via Abstract Interpretation
POPL
Stephen Mell University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania