Undecidability of Dyadic First-Order Logic in Coq. - Johannes Hostert; Andrej Dudenhefner; Dominik Kirst (ITP, 2022)

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. - Armaël Guéneau; Johannes Hostert; Simon Spies; Michael Sammler; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Tree Borrows. - Neven Villani; Johannes Hostert; Derek Dreyer; Ralf Jung 002 (Proc. ACM Program. Lang., 2025)