| 2023 | CRYPTO | Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. | Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grgoire, Yu-Hsuan Huang, Andreas Hlsing, Yi Lee, Xiaodi Wu |
| 2021 | ITP | A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. | Christian Doczkal |
| 2020 | CPP | Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. | Christian Doczkal, Damien Pous |
| 2018 | CPP | Completeness and decidability of converse PDL in the constructive type theory of Coq. | Christian Doczkal, Joachim Bard |
| 2018 | ITP | A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. | Christian Doczkal, Guillaume Combette, Damien Pous |
| 2018 | MFCS | Treewidth-Two Graphs as a Free Algebra. | Christian Doczkal, Damien Pous |
| 2016 | ITP | Two-Way Automata in Coq. | Christian Doczkal, Gert Smolka |
| 2015 | ITP | Transfinite Constructions in Classical Type Theory. | Gert Smolka, Steven Schfer, Christian Doczkal |
| 2014 | ITP | Completeness and Decidability Results for CTL in Coq. | Christian Doczkal, Gert Smolka |
| 2013 | CPP | A Constructive Theory of Regular Languages in Coq. | Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka |
| 2012 | CPP | Constructive Completeness for Modal Logic with Transitive Closure. | Christian Doczkal, Gert Smolka |
| 2011 | CPP | Constructive Formalization of Hybrid Logic with Eventualities. | Christian Doczkal, Gert Smolka |