How We Built Cedar: A Verification-Guided Approach [pdf]
Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah^†, Emina Torlak, Andrew Wells.
FSE 2024.

ViCAR: Visualizing Categories with Automated Rewriting in Coq [pdf]
Bhakti Shah*, William Spencer*, Laura Zielinski*, Adrian Lehmann, Ben Caldwell, Robert Rand .
ACT 2024.

VyZX: Formal Verification of a Graphical Quantum Language [pdf]
Adrian Lehmann*, Ben Caldwell*, Bhakti Shah, Robert Rand.
TBA.

Imperative Syntax for Dependent Types [pdf]
Bhakti Shah, Edwin Brady.
HATRA 2025.

VyZX: Formal Verification of a Graphical Quantum Language with automated structural rewrites [pdf]
Adrian Lehmann*, Ben Caldwell*, Bhakti Shah, Robert Rand.
QPL 2024.

Visualizing Graphical Proofs in Coq [extended abstract] [poster]
Bhakti Shah.
ICFP 2023 SRC, 🏆 Second Place (Undergraduate).

Integrating Dependency Building with Document Checking in Coq [extended abstract]
Emilio Jesús Gallego Arias, Bhakti Shah.
CoqPL 2024.

A Lean Formalization of Cedar [extended abstract] [poster]
Bhakti Shah.
POPL 2024 SRC, 🏆 Second Place (Undergraduate).

Proof Visualization for Graphical Languages [pdf] [slides]
Bhakti Shah.
Master's Thesis, University of Chicago.