Certifying graph-manipulating C programs via localizations within data structures. - Shengyi Wang; Qinxiang Cao; Anshuman Mohan; Aquinas Hobor (Proc. ACM Program. Lang., 2019)

A functional proof pearl: inverting the Ackermann hierarchy. - Linh Tran; Anshuman Mohan; Aquinas Hobor (CPP, 2020)

Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms. - Anshuman Mohan; Wei Xiang Leow; Aquinas Hobor (CAV (2), 2021)

Formal Abstractions for Packet Scheduling. - Anshuman Mohan; Yunhe Liu 002; Nate Foster; Tobias Kappé; Dexter Kozen (Zenodo, 2023)

Formal Abstractions for Packet Scheduling. - Anshuman Mohan; Yunhe Liu 002; Nate Foster; Tobias Kappé; Dexter Kozen (Proc. ACM Program. Lang., 2023)

Unifying Static and Dynamic Intermediate Languages for Accelerator Generators. - Caleb Kim; Pai Li; Anshuman Mohan; Andrew Butt; Adrian Sampson; Rachit Nigam (Proc. ACM Program. Lang., 2024)