| 2025 | CADE | SMT and Functional Equation Solving over the Reals: Challenges from the IMO. | Chad E. Brown, Karel Chvalovsk, Mikols Janota, Mirek Olsk, Stefan Ratschan |
| 2024 | IJCAR | Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. | Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk |
| 2024 | ITP | A Formal Proof of R(4, 5)=25. | Thibault Gauthier, Chad E. Brown |
| 2024 | LPAR | Experiments with Choice in Dependently-Typed Higher-Order Logic. | Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk |
| 2023 | ITP | Automated Theorem Proving for Metamath. | Mario Carneiro, Chad E. Brown, Josef Urban |
| 2023 | LPAR | A Mathematical Benchmark for Inductive Theorem Provers. | Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban |
| 2023 | LPAR | Experiments on Infinite Model Finding in SMT Solving. | Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk |
| 2022 | CADE | Lash 1.0 (System Description). | Chad E. Brown, Cezary Kaliszyk |
| 2022 | CAV | Proofgold: Blockchain for Formal Methods. | Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban |
| 2020 | CADE | Prolog Technology Reinforcement Learning Prover - (System Description). | Zsolt Zombori, Josef Urban, Chad E. Brown |
| 2020 | CPP | Exploration of neural machine translation in autoformalization of mathematics in Mizar. | Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban |
| 2019 | CADE | GRUNGE: A Grand Unified ATP Challenge. | Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban |
| 2019 | ITP | Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. | Chad E. Brown, Cezary Kaliszyk, Karol Pak |
| 2016 | CADE | Internal Guidance for Satallax. | Michael Frber, Chad E. Brown |
| 2013 | CADE | From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. | Chad E. Brown, Christine Rizkallah |
| 2012 | CADE | Satallax: An Automatic Higher-Order Prover. | Chad E. Brown |
| 2011 | CADE | Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. | Chad E. Brown |
| 2010 | CADE | Analytic Tableaux for Higher-Order Logic with Choice. | Julian Backes, Chad E. Brown |
| 2009 | CADE | Progress in the Development of Automated Theorem Proving for Higher-Order Logic. | Geoff Sutcliffe, Christoph Benzmller, Chad E. Brown, Frank Theiss |
| 2009 | TABLEAUX | Terminating Tableaux for the Basic Fragment of Simple Type Theory. | Chad E. Brown, Gert Smolka |
| 2006 | CADE | Cut-Simulation in Impredicative Logics. | Christoph Benzmller, Chad E. Brown, Michael Kohlhase |
| 2006 | CADE | Combining Type Theory and Untyped Set Theory. | Chad E. Brown |
| 2005 | CADE | Reasoning in Extensional Type Theory with Equality. | Chad E. Brown |
| 2002 | CADE | Solving for Set Variables in Higher-Order Theorem Proving. | Chad E. Brown |
| 2000 | CADE | Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. | Peter B. Andrews, Chad E. Brown |
| 2000 | CADE | System Description: TPS: A Theorem Proving System for Type Theory. | Peter B. Andrews, Matthew Bishop, Chad E. Brown |