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.

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.