[POPL 2016] - Dependent Types and Multi-monadic Effects in F⭑

[POPL 2017] - Dijkstra Monads for Free

[POPL 2018] - Recalling a Witness: Foundations and Applications of Monotonic State

[ESOP 2019] - Meta-F⭑: Proof Automation with SMT, Tactics, and Metaprograms

[ICFP 2020] - SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs

[ICFP 2021] - Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic