Preprint (pdf), Sep 2025

Abstract: Railroad diagrams (also called “syntax diagrams”) are a common, intuitive visualization of grammars, but limited tooling and a lack of formal attention to their layout mostly confines them to hand-drawn documentation. We present the first formal treatment of railroad diagram layout along with a principled, practical implementation. We characterize the problem as compiling a diagram language (specifying conceptual components and how they connect and compose) to a layout language (specifying basic graphical shapes and their sizes and positions). We then implement a compiler that performs line wrapping to meet a target width, as well as vertical alignment and horizontal justification per user-specified policies. We frame line wrapping as an optimization problem, where we describe principled dimensions of optimality and implement corresponding heuristics. For front-end evaluation, we show that our diagram language is well-suited for common applications by describing how regular expressions and Backus-Naur form can be compiled to it. For back-end evaluation, we argue that our compiler is practical by comparing its output to diagrams laid out by hand and by other tools.

Short paper (web, pdf) at the SPLASH 2025 Doctoral Symposium, Singapore

Abstract: Diagrams are rare and hard to work with in programming and theorem-proving environments. Existing diagramming systems do not meet the practical needs of interactive, exploratory use, such as keeping diagrams understandable as they grow in size with limited screen space, or as they evolve as the user steps through the program or proof. My research seeks to develop an approach—compositional diagramming—that meets these needs. Diagrams are formed of independent parts composed in systematic ways reflecting the structure of the represented object, and the diagramming system compiles a higher-level description of the object to lower-level diagram components. Techniques that make diagrams more practical, such as wrapping, folding, and packing, fit neatly into a compositional approach. Through my work, I hope to build a useful diagramming system for working computer scientists, mathematicians, and programmers, based on a better understanding of compositional diagrams.

Paper (pdf), presentation (YouTube). This was a workshop paper at HATRA 2023 (Human Aspects of Types and Reasoning Assistants), colocated with SPLASH, Cascais, Portugal.

Abstract: Diagrams are ubiquitous in the development and presentation of proofs, yet surprisingly uncommon in computerized mathematics. Instead, authors and developers rely almost exclusively on line-oriented notations (textual abbreviations and symbols). How might we enrich interactive theorem provers with on-the-fly visual aids that are just as usable? We answer this question by identifying a key challenge: designing declarative languages for composable diagram templates, that provide good-looking implementations of common patterns, and allow for rapid prototyping of diagrams that remain stable across transformations and proof steps.

My Spring 2023 “semester project” in the Systems and Formalisms laboratory (SYSTEMF), which ends with the academic semester only for administrative reasons, so this is ongoing work. My report is available in web and pdf formats.

Abstract: We make the case for better diagramming tools that exploit the regular, compositional structure of diagrams often used in computer science to allow the diagrammer to easily describe diagrams at a higher level of abstraction than existing drawing programs, and compute with them as first-class objects through natural APIs, without compromising on their aesthetic quality. The ability to programmatically produce pretty illustrations would greatly enrich programming environments and proof assistants. We motivate this vision with two case studies of diagram domains, for which we describe the beginnings of diagrammatic theories as well as our prototype implementations. We discuss what these case studies reveal about the theory and practice of general-purpose diagramming.

Work I did in the Programming Methods Laboratory (LAMP) or “the Scala lab” at EPFL in 2022–23. I wrote a technical report (web, pdf) about it.

Abstract: I describe work towards an interpreter for TASTy, a high-level binary interchange format for Scala 3, motivated by the desire for a specification for the format independent of the compiler. I explain some core implementation details and summarize the current state of the project and avenues for future work, particularly regarding JavaScript interoperability and the Scala.js standard library. I also describe a subsidiary project, TASTyViz, a web-based TASTy visualizer motivated by the absence of human interfaces for TASTy. I conclude by reflecting on the challenges and takeaways of this project.

A project I conducted as an undergraduate with Clément Pit-Claudel and Adam Chlipala in the Programming Languages and Verification lab (PLV) at MIT CSAIL. We had a workshop paper and talk at CoqPL 2021.

Abstract: We demonstrate correct-by-construction firewalls—stateful packet filters for TCP/IP packets—using the Fiat synthesis library. We present a general DSL for specifying their behavior independent of algorithmic implementation. We outline the design of a verified compiler in Coq, detail a few verified efficiency optimizations, and show how the compiler can easily be extended to support custom optimizations for user-defined policies.

TA in Fall 2023, Fall 2024, Fall 2025. Coauthored a practice paper (web, pdf) about the design of the course for SEFI 2024 (52nd Annual Conference of the European Society for Engineering Education). Awarded the EPFL IC Teaching Assistant Award in 2024.

I helped bootstrap the course in 2023, and I was heavily involved in its overall administration in 2023 and 2024, including managing a staff of around 20 Bachelor’s, Master’s, and PhD students; tracking design, testing, release, and bug-fixes for assignments and exams; and designing materials distributed to over 400 second-year students taking the course. I mentored a Master’s student in 2024 to take over many of these responsibilities in 2025.

TA in Spring 2023, Spring 2024.

Undergrauate TA (UTA) in Fall 2021 and Spring 2022, lab assistant (LA) in Spring 2021. Awarded the MIT EECS Undergraduate Teaching Assistant (UTA) Award for Teaching Excellence in 2022.

I gained a lot of experience helping students 1-on-1 to solve and debug extensive weekly lab assignments (in Python) covering fundamental programming concepts like recursion, graph search, linked lists / trees / other common data structures, and object-oriented programming. I also piloted a new approach to staff training by designing training materials for each assignment showing common bugs, bad coding habits, alternative solutions, etc., often drawn from real student submissions from previous semesters. My materials took inspiration from Pólya’s four steps for How to Solve It in training staff to guide students towards resolving their issues.

A course about the mathematics of music that I’ve taught in various forms with Andrew Lin and Mandar Juvekar, primarily to high-schoolers at MIT ESP programs. I am in the process of developing some materials including demos with Max.

Course description: "Why do musicians like ‘thirds’, ‘fourths’, and ‘fifths’? Why does the same note played on a violin and a trombone sound so different? Are all pianos secretly out of tune? What is a polyrhythm? How can a trumpet produce all the notes with only three valves? Come learn about the mathematics of music behind all these questions. A little bit of music theory and math can go a long way in understanding the structure of music in a totally new way. Expect to do a lot of careful listening as you develop your musical mind!"

Topics include logic, meta-mathematics, and Gödel’s theorem; formal methods and the Curry-Howard isomorphism; combinatorial game theory; musical tuning and temperament; math contest problem-solving with recurrence relations, generating functions, and the pigeonhole principle. Audiences were mainly advanced high-schoolers or undergraduates.

Apertium is an open-source platform for rule-based (i.e. not machine learning) machine translation, with particular applications to low-resource languages and related language pairs. Apertium provides tools to build translation pipelines from morphological databases, bidirectional dictionaries, etc. and to serve such pipelines on the web, and also provides some translation pipelines itself. I contributed to the project from 2014 to 2018, mostly working on web infrastructure, and I won the Google Code-In Grand Prize in 2017 for my work.

Sushain Cherivirala, me, Jonathan North Washington, and Kevin Brubeck Unhammer had a workshop paper at the Workshop on Technologies for Machine Translation of Low Resource Languages (LoResMT) 2018, where I presented our work (slides). I also wrote a technical report about my main contributions (overlaps with the paper above).

In January 2020, I was a research assistant/intern to Prof. Tobias Gerstenberg in the Causality in Cognition lab (CICL) at Stanford. I contributed to a project to understand how, cognitively, humans judge an event (or its absence) to have caused another. One model involves counterfactual simulation, i.e. simulating what would have happened if the prior event had not (or had) occurred to judge how likely the posterior event would have been. I worked on modeling such probabilistic simulations on a computer and analyzing how well they fit the results of human experiments. This project could be considered to be in the intersection of (computational) cognitive science and ‘experimental philosophy’.

Tobias Gerstenberg and Simon Stephan later published a journal paper including this and other work in Cognition in 2021.