Voting Theory in the Lean Theorem Prover. - Wesley H. Holliday; Chase Norman; Eric Pacuit (LORI, 2021)

PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency. - Chase Norman; Adwait Godbole; Yatin A. Manerkar (ASPLOS (3), 2023)

Program Synthesis in Saturation. - Petra Hozzová; Laura Kovács; Chase Norman; Andrei Voronkov (CADE, 2023)

Canonical for Automated Theorem Proving in Lean. - Chase Norman; Jeremy Avigad (CoRR, 2025)