| 2025 | ITP | A Certified Proof Checker for Deep Neural Network Verification in Imandra. | Remi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, Guy Katz |
| 2025 | ITP | Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk). | Kathrin Stark |
| 2024 | ITP | Taming Differentiable Logics with Coq Formalisation. | Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark |
| 2023 | LOPSTR | Towards a Certified Proof Checker for Deep Neural Network Verification. | Remi Desmartin, Omri Isac, Grant O. Passmore, Kathrin Stark, Ekaterina Komendantskaya, Guy Katz |
| 2023 | LPAR | Logic of Differentiable Logics: Towards a Uniform Semantics of DL. | Natalia Slusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert J. Stewart, Kathrin Stark |
| 2020 | CPP | Coq la carte: a practical approach to modular syntax with binders. | Yannick Forster, Kathrin Stark |
| 2019 | CPP | Call-by-push-value in coq: operational, equational, and denotational theory. | Yannick Forster, Steven Schfer, Simon Spies, Kathrin Stark |
| 2019 | CPP | Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. | Kathrin Stark, Steven Schfer, Jonas Kaiser |
| 2018 | CPP | Binder aware recursion over well-scoped de Bruijn syntax. | Jonas Kaiser, Steven Schfer, Kathrin Stark |
| 2016 | ITP | Hereditarily Finite Sets in Constructive Type Theory. | Gert Smolka, Kathrin Stark |