Automatic Generation of Diagrams for Category-theoretic Proofs in Agda. Kelton OBrien. [Slides coming soon!] (Presentation, MWPLS 2024)
The Nerve of a Category. Kelton OBrien. [PDF] (Bachelor's Capstone Thesis[1], 2024)
Guiding Greybox Fuzzing with Mutation Testing. Vasudev Vikram, Isabella Laybourn, Ao Li, Nicole Nair, Kelton OBrien, Rafaello Sanna, and Rohan Padhye. [PDF|ACM dl] (Paper, ISSTA 2023) Distinguished paper award!
I am currently working on exactly what is said on the tin, utilizing the 1Lab library for cubical Agda and Agda reflection to generate commutative diagrams from types, thinning the gap between graphical reasoning on paper and textual reasoning in a proof assistant (at least to some degree).
Right now, univalent type theories can be a bit of a pain to work with. The homotopical structure in the equalities provide a lot of extra complexity to juggle when we only sometimes want it, Glue types in Cubical Type Theory are famously difficult/annoying to work with, the homotopy theoretic ideas can be a lot to digest if you aren't a mathematician, etc. It seems that there are two problems: the type theories themselves, and the tools we use to interact with them. It appears to me that we should be able to craft type theories that have univalence but do not suffer from some these issues (like glue types). There's some work on this idea already with things like Higher Observational Type Theory, but the are has a lot to be explored! Likewise, there seems that some of these problems could be better handled by a proof assistant that just has better univalent specific proof automation. It seems like a proof assistant that has a better understanding of things like h-levels could automate away a lot of the problems that we run into when proving things formally with univalent type theories.
Currently I am working on formalizing mathematics with homotopy type theory based on work I did when I was advised by Favonia. For this, I am currently working on formalizing two different subjects: The theory of lie groups and their representations, and group cohomology.
After going through the literature I noticed that there actually hasn't been much in terms of formalization for Lie groups and representation theory. This makes sense to a degree, lie groups and representations tend to be a more in the linear algebra weeds than is natural to express with homotopy type theory. That all said, differential cohesive type theory (and modal HoTT more generally) provides a solid way of connecting these more bits-and-bobs notions to our synthetic notions with some elegance. This has mostly been used to do formalization for differential geometry, so connecting lie theory to the more synthetic/homotopical side of things (will be) a novel contribution.
I am also working on formalizing group cohomology in cubical Agda. This is more in line with the other work of formalization of algebraic topology in HoTT than the previous topic, but is an important topic in homological algebra that hasn't been formalized to my understanding. Urs schreiber (et. al.) however do provide infinity-topos theoretic (read: HoTT-theoretic) analysis of group cohomology on paper that is summarized on the n-lab page for group cohomology.
I'm also working with Soha Hussein, Steven McCamant, and Favonia of the UMN on formalizing and proving the correctness of Java Ranger, a system that uses a novel approach to merging paths for more effecient symbolic execution.
Summer 2023 I worked at Microsoft Research on TLA+, a temporal logic for specifying, verifying, and model checking algorithms. There I extended TLA+ to be able to reason about probabilities and particular lengths of time. In TLA+, one can generally only reason in absolutes. Either something occurs or it does not. There is no notion of probability, and no way to talk about how long something takes, so reasoning about probabilistic programs, or even the performance of a system directly is impossible (how do you deal with message loss? Likelyhood of particular operations in real world usage?). My contribution was to create a new temporal logic based on TLA+, extend it with new temporal and probabilistic operators to be able to reason about and verify these properties. I also wrote a transpiler from this new temporal logic to TLA+, which uses a novel algorithm to determine the number of runs required from the statistical model checking verification. This ends up being very difficult due to some properties of TLA+ (mainly its linearity), but with some clever optimizations and work-arounds, it still ends up being a powerful reasoning and verification tool. One thing that's special about TLA+ is that it is a very usable system --- Markus Kuppe teaches a TLA+ workshop that only takes a couple days and teaches you pretty much everything you need to know. Because you foward most of the complexity of verification to model checking, the verifier can focus just on writing specifications and properties they want to verify. My extensions to the system perserve this (I would say); I only add 2 new operators to the language, and a couple rules specifying how they can interact.
The summer of 2022 I did an REU at Carnegie Mellon, where I worked on mu2 with Rohan Padhye. Mu2, is a mutation analysis based fuzzer designed to to generate test cases. Fuzzers work by generating lots of inputs to a program, mutating old inputs to generate new inputs, and saving them if they increase code coverage. Fuzzers have been traditionally used for finding bugs in programs, but a set of inputs that has high code coverage also serves as a good test suite! Along this line, Mu2 improves fuzzers as tools for generating test suites by also keeping track of mutation score as a metric, a measure that is used for assessing the quality of the tests. This is a very expensive operation which requires the program to be run hundreds of times instead of just once, so my work involved optimizing Mu2 with dynamic analysis. You can check out the paper covering Mu2 above.
At MELT, I worked on the copper parser generator. My work consisted of implementing the paper Finding Counterexamples from Parsing Conflicts by Isradisaikul and Myers for Copper. I worked on this project very early on in my research career (specifically when I was 18), so this was my introduction to parsing, and the research process in general. This was a large project that touched a lot of the LALR parsing apparatus, and significantly improved usability of the parser and all tools that use it. Copper is used in the PL course at UMN, and these changes have made it so that the students can focus on the important ideas, rather than the details of the LALR parsing algorithm.
[1]: This was basically a smaller, less research intensive version of a bachelor's thesis that was required of mathematics B.A students. [back to location]