Anshuman Mohan

Gates 407 · amohanⓐcs.cornell.edu

Capra ·
Ctrl-Alt
·
Middle Sister

I am a PhD candidate at Cornell University's Department of Computer Science. My research is in programming languages.

With Adrian Sampson and others, I work on Pollen, a DSL-to-hardware compiler with applications to pangenomics. With Nate Foster and others, I work on programmable packet scheduling. With James Grimmelmann and others, I think about how computer science intersects with the law.

Before Cornell, I worked with Aquinas Hobor and others on CertiGraph, a Coq development for the formal verification of graph-manipulating programs written in C. Before Aquinas, I was part of the inaugural cohort of Yale-NUS College. I gave the commencement address for my graduating class.

Personal

Science is for everyone, but scientific papers are not. 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

Formal Abstractions for Packet Scheduling

Mohan, Liu, Foster, Kappé, Kozen
OOPSLA 2023, Cascais

🎉 Distinguished Paper Award 🎉

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

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

Mohan, Leow, Hobor
CAV 2021, Online

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 Coq.

Functional Proof Pearl:
Inverting the Ackermann Hierarchy

Tran, Mohan, Hobor
CPP 2020, New Orleans

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 Coq, 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

Wang, Cao, Mohan, Hobor
OOPSLA 2019, Athens

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 Coq library that provides a setup for defining mathematical graphs in Coq, 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 Coq.

Service

External Reviewer

Instructor

Fall 2023: CS 6006: Succeeding in the Graduate
Environment

Summer 2022: New York State's 4H CareerEx program

Spring 2022: Cornell's Grasshopr
program