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