Hereditarily Finite Sets in Constructive Type Theory. - Gert Smolka; Kathrin Stark (ITP, 2016)

Binder aware recursion over well-scoped de Bruijn syntax. - Jonas Kaiser; Steven Schäfer; Kathrin Stark (CPP, 2018)

Call-by-push-value in coq: operational, equational, and denotational theory. - Yannick Forster 002; Steven Schäfer; Simon Spies; Kathrin Stark (CPP, 2019)

Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. - Kathrin Stark; Steven Schäfer; Jonas Kaiser (CPP, 2019)

POPLMark reloaded: Mechanizing proofs by logical relations. - Andreas Abel 001; Guillaume Allais; Aliya Hameer; Brigitte Pientka; Alberto Momigliano; Steven Schäfer; Kathrin Stark (J. Funct. Program., 2019)

Coq à la carte: a practical approach to modular syntax with binders. - Yannick Forster 002; Kathrin Stark (CPP, 2020)

Mechanising syntax with binders in Coq. - Kathrin Stark (2020)

Towards a Certified Proof Checker for Deep Neural Network Verification. - Remi Desmartin; Omri Isac; Grant O. Passmore; Kathrin Stark; Ekaterina Komendantskaya; Guy Katz (LOPSTR, 2023)

Logic of Differentiable Logics: Towards a Uniform Semantics of DL. - Natalia Slusarz; Ekaterina Komendantskaya; Matthew L. Daggitt; Robert J. Stewart 001; Kathrin Stark (LPAR, 2023)

Taming Differentiable Logics with Coq Formalisation. - Reynald Affeldt; Alessandro Bruni; Ekaterina Komendantskaya; Natalia Slusarz; Kathrin Stark (ITP, 2024)

A Certified Proof Checker for Deep Neural Network Verification. - Remi Desmartin; Omri Isac; Ekaterina Komendantskaya; Kathrin Stark; Grant O. Passmore; Guy Katz (CoRR, 2024)

A Verified Foreign Function Interface between Coq and C. - Joomy Korkut; Kathrin Stark; Andrew W. Appel (Proc. ACM Program. Lang., 2025)