Anshuman Mohan (original) (raw)
Anshuman Mohan
News
Fall 2025
After a year of teaching, I am excited to return to research full-time!
Summer 2025
I spend the summer with HPE Labs in the Bay Area, working with Jean Tourrilhes, Bob Lantz, and Puneet Sharma.
Spring 2025
Fall 2024
Summer 2024
I mentored three extraordinary undergraduate students through Cornell's BURE program. I also ran the Academic Skills Seminar Series for the entire 60-person BURE cohort.
Spring 2024
I accepted an additional appointment at Cornell's West Campus Housing System. I am now a Graduate Resident Fellow at Flora Rose House.
Fall 2023
I took Formal Abstractions on tour! I was at Open Universiteit Nederland in Heerlen, OOPSLA in Cascais, NYU in New York City, MIT in Cambridge, UW in Seattle, and Inria in Rennes.
I ran a new graduate course, CS 6006 Succeeding in the Graduate Environment, for its first iteration. The Department recognized my work with its inaugural Outstanding Service Award.
Personal
Science is for everyone, but scientific papers tend not to be. My blog is a humble experiment in accessibility: I offer primers on research topics I care about, assuming no prior exposure to computer science. Because I cannot help myself, I will probably also write about food.
To plant a garden do scientific research is to believe in tomorrow
Part of the point of doing science is to have your work seen, used, and made redundant. Sadly, at the rate we're heating the planet, we'll soon have more rudimentary things to worry about. I'm cautiously optimistic about climate change, but with the understanding that intentional work is needed from everyone who can afford to put it in. I'm still working on my plan, so please reach out if you'd like to discuss this as either a mentor or a coconspirator.
Publications
Unifying Static and Dynamic Intermediate Languages for Accelerator Generators
Kim, Li, Mohan, Butt, Sampson, Nigam
OOPSLA 2024, Pasadena
Slides ·Paper · Code merged into Calyx
Compilers for accelerator design languages translate high-level languages into application-specific hardware. These compilers rely on a control interface to compose hardware units. There are two choices: static control, which relies on cycle-level timing; and dynamic control, which uses explicit signalling to avoid depending on timing details. Static control is efficient but brittle; dynamic control incurs hardware costs to support compositional reasoning. We present a compiler that unifies static and dynamic control in a single intermediate language, and yields rich dividends. Our key observation is that the schedule that can be generated using static control is merely a refinement of the schedule that can be generated using dynamic control. We can thus optimize code by combining facts from static and dynamic submodules, and can opportunistically convert code from dynamic to static control styles.
Formal Abstractions for Packet Scheduling
PIFO trees are an exciting primitive for programmable packet scheduling, but are poorly understood and underutilized. Part of the issue is that the expressivity of a PIFO tree is thought to be inextricably tied to its shape, meaning that expressing a range of scheduling policies would require a range of tree-shapes to be deployed in hardware. This is clearly untenable. In our work, we give PIFO trees a formal syntax and semantics, prove properties about the expressivity of PIFO trees as a function of their shape, and show how to break free of the connection between shape and expressivity. This comes together as a compiler that allows one to write a program — a scheduling algorithm — against one PIFO tree but still deploy it on another PIFO tree of a different shape. If a sufficiently expressive PIFO tree is made available in hardware, our compiler can allow a range of scheduling policies to run on it.
Littleton: An Educational Environment for Property Law and Legal Calculi
Basu, Mohan, Grimmelmann, Foster
ProLaLa 2022, Philadelphia
While much of the law is up to human interpretation, property law has a more programmatic goal. An item is conveyed from person to person, and this conveyance may be affected by further conveyances, life events such as birth and death, and the satisfaction or dissatisfaction of arbitrary stipulations placed by conveyors. Through all of this, the law desires unambiguous ownership. Orlando is a DSL that addresses this problem through a novel use of techniques from PL, and Littleton is an interpreter that makes these techniques pedagogically useful.
Functional Correctness of C Implementations of Dijkstra's, Prim's, and Kruskal's Algorithms
We extend the CertiGraph library to enable reasoning about labeled edges and undirected graphs, and use it to verify C implementations of Dijkstra's, Prim's, and Kruskal's algorithms. Each of these classic algorithms has been used and studied for more than 60 years, and yet our verification reveals remarkable subtleties. We show that Dijkstra has an overflow issue that places delicate restrictions on the maximum allowable path cost. We also debunk the universal misconception that Prim runs correctly only on connected graphs. Our proofs are checked in Rocq.
Functional Proof Pearl: Inverting the Ackermann Hierarchy
The Ackermann function \(\mathcal{A}\) grows explosively, and its inverse \(\alpha\) is of interest in CS. Sadly, the standard practice of computing \(\alpha\) via \(\mathcal{A}\) is untenable. We give a new and efficient computation of \(\alpha\). We also give efficient computations for the related and better-known hyperoperation hierarchy(\(+\), \(\times\), exp, tetration, etc) and its inverse(\(-\), \(\div\), log, log\(^{*}\), etc). Our definitions are proved correct in Rocq, and our time bounds are supported by pen-and-paper proofs and benchmarks after extraction to OCaml.
Certifying Graph-Manipulating C Programs via Localizations within Data Structures
Formally verifying graph algorithms is hard: nodes can be shared arbitrarily, so uninvolved subgraphs cannot be "framed away". We address this with a new separation logic rule called localize. We develop CertiGraph, a Rocq library that provides a setup for defining mathematical graphs in Rocq, laying them out in memory via separation logic, and stating and proving properties about them. We demonstrate the power of CertiGraph by using it to verify seven graph-manipulating C programs. Our flagship example is a generational garbage collector. We identify two places where the semantics of C is too restrictive to define OCaml-style GCs. Our proofs are checked in Rocq.
Teaching
Instructor of Record
K-12 Outreach
Service
K-12 Outreach
External Reviewer