Three papers and keynote by CSE researchers at SPLASH 2024

CSE researchers are presenting three papers at the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH). A top international venue for new research spanning software construction and delivery and programming languages, SPLASH combines several SIGPLAN conferences including OOPSLA, SAS, GPCE, and SLE, as well as several other workshops and events. This year’s conference is taking place October 20-25 in Pasadena, CA.

Papers by CSE authors at SPLASH cover a range of topics at the intersection of programming languages and software, including SQL query equivalence checking, classroom proof assistants, and leveraging AI for code completion and error correction.

In addition to the new papers being presented at SPLASH, Cyrus Omar delivered the keynote lecture at the Human Aspects of Types and Reasoning Assistants (HATRA) workshop on Sunday, October 20, his talk titled  “Research Methods for Designing Next-Generation Programming Systems.” Omar discussed exciting new trends in programming experience design research, such as live programming, direct manipulation interfaces, AI for coding, collaborative editing, and more, while also emphasizing the variety of methods that can be used to break new ground in this area.

The papers appearing at the conference are as follows, with the names of CSE-affiliated authors in bold:

VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints (OOPSLA ‘24) *Distinguished Paper Award*
Yang He, Pinhan Zhao, Xinyu Wang, Yuepeng Wang

Abstract: The task of SQL query equivalence checking is important in various real-world applications (including query rewriting and automated grading) that involve complex queries with integrity constraints; yet, state-of-the-art techniques are very limited in their capability of reasoning about complex features (e.g., those that involve sorting, case statement, rich integrity constraints, etc.) in real-life queries. To the best of our knowledge, we propose the first SMT-based approach and its implementation, VeriEQL, capable of proving and disproving bounded equivalence of complex SQL queries. VeriEQL is based on a new logical encoding that models query semantics over symbolic tuples using the theory of integers with uninterpreted functions. It is simple yet highly practical — our comprehensive evaluation on over 20,000 benchmarks shows that VeriEQL outperforms all state-of-the-art techniques by more than one order of magnitude in terms of the number of benchmarks that can be proved or disproved. VeriEQL can also generate counterexamples that facilitate many downstream tasks (such as finding serious bugs in systems like MySQL and Apache Calcite).

Statically Contextualizing Large Language Models with Typed Holes (OOPSLA ‘24)
Andrew Blinn, Xiang Li, June Hyung Kim, Cyrus Omar

Abstract: Large language models have changed the landscape for code completion, but the techniques by which prompts are constructed and model responses are handled fail to fully leverage the wealth of structured semantic information available to modern language servers and from there, IDEs. We contend that AIs need IDEs, too! This paper integrates LLMs into the Hazel Assistant, which uses static retrieval and error correction techniques driven by the Hazel Language Server. The Hazel Language Server is able to identify types and typing contexts for holes in program sketches, with total error correction ensuring that a semantically meaningful program sketch is always available. This allows for semantic contextualization with information that is not lexically local to the cursor, but is semantically local to the programmer’s intent as expressed through the type system. Contextualized model completions are then iteratively refined via dialog with a language server, providing static error correction. To validate these methods, we present MVUBench, a dataset of MVU applications written in Hazel and TypeScript, particular suited to contrast methods of static retrieval and contextualization. Further, we duplicate our methods and test suite in TypeScript in order to validate the applicability of these methods to higher-resource mainstream languages.

Learner-Centered Design Criteria for Classroom Proof Assistants (HATRA ‘24)
Matthew Keenan, Cyrus Omar

Abstract: We survey publications that report on the experience of introducing proof assistants into classrooms, identifying observed advantages and challenges. From this, we synthesize a series of design criteria for classroom proof assistants, and suggest methods for evaluating future designs against these criteria. Finally we discuss how we are using these criteria to guide design decisions in ongoing work on designing the Hazel Prover.