Publications
Staged Specification Logic for Verifying Higher-Order Imperative Programs
Specification and Verification for Unrestricted Algebraic Effects and Handling
Protocol Conformance with Choreographic PlusCal
Automated Temporal Verification for Algebraic Effects
Tracing OCaml Programs
Automating Continuous Planning in SAFe
The Dynamics of Software Composition Analysis
Efficient Static Checking of Library Updates
SGL: A DSL for large-scale analysis of open-source code
Higher-Order Debugging and Logging for OCaml