Research
Duper: An Automatic Theorem Prover for Dependent Type Theory
One of the most important factors impacting the usability of an interactive theorem prover (ITP) is the power of its automation. For example, in Isabelle/HOL, the general purpose automation provided by Metis and Sledgehammer has become an essential part of the typical user's workflow.
Most current ITP automation is either targeted to a particular domain or designed primarily for first-order logic. But most ITPs support languages much richer than that of first-order logic. My research with Yicheng Qian and Alexander Bentkamp concerns general-purpose ITP automation designed to effectively operate in Lean's dependently typed setting. Together we are developing Duper, an automatic theorem prover in Lean 4 based on the superposition calculus. To learn more about Duper, feel free to read this conference paper.
A Formalized Reduction of Keller's Conjecture
If you attempted to entirely cover a 2-dimensional Euclidean plane with non-overlapping unit squares, you would quickly find that it is necessary to have at least two squares share a complete edge. Similarly, if you attempted to fill a 3-dimensional Euclidean space with non-overlapping unit cubes, you would find that it is necessary to have at least two cubes share a complete face.
Keller's Conjecture states that this trend holds in arbitrary dimensions. As it turns out, Keller's Conjecture is true in 7 or fewer dimensions, and is false in 8 or more dimensions.
The proof that Keller's Conjecture holds in 7 dimensions critically relies on a reduction from the original geometric conjecture to a finite graph clique problem. My research involved using the Lean 3 theorem prover to formalize and verify this reduction. I also used this formalized reduction to produce the first verified proof that Keller's Conjecture is false in 8 dimensions. You can read more about this work here, and you can check out the formal proofs here.
A Polymorphic Logical Framework
The LF logical framework is a formal system designed to provide a general means of presenting deductive systems. But the ease with which a logical framework can present certain deductive systems and support various applications depends significantly on the language features provided by that framework. For this reason, attention has been given to areas in which LF can be improved for certain applications, yielding extensions to LF such as LLF (a linear logical framework), RLF (a logical framework for relevant logics), and CLF (a concurrent logical framework).
My research with Karl Crary involved developing an extension to LF that supports representing and reasoning about polymorphic types. The primary aims for this work were to define the extension’s type system and semantics, validate it by proving that the system honors identity expansion and cut admissibility, and potentially formalize the extension and the proofs that validate it in Coq.
Program Equivalence for Assisted Grading of Functional Programs
In courses that involve programming assignments, giving meaningful feedback to students is an important challenge. In a perfect world, every student would receive personalized human feedback. But as computer science courses grow in demand, this ideal is increasingly costly.
To make human feedback more accessible, even as class sizes grow considerably, I worked with Vijay Ramamurthy, Ruben Martins, and Umut Acar to create Zeus. Zeus is a tool that can take a set of programs written in Standard ML, and, using the SMT solver Z3, partition them into buckets of provably equivalent programs. This makes it possible to simultaneously give human feedback to all students that implemented the same algorithm or made the same error.
To learn more about how Zeus is designed, and how it can be used to make human feedback more accessible, feel free to watch my OOPSLA talk embedded above. For more information on Zeus' theoretical foundations, you can read our conference paper here and its extended version here.