Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal. - Christian Doczkal; Jan Schwinghammer (LFMTP, 2009)

Strong Normalization of Moggis's Computational Metalanguage. - Christian Doczkal (Arch. Formal Proofs, 2010)

Constructive Formalization of Hybrid Logic with Eventualities. - Christian Doczkal; Gert Smolka (CPP, 2011)

Constructive Completeness for Modal Logic with Transitive Closure. - Christian Doczkal; Gert Smolka (CPP, 2012)

A Constructive Theory of Regular Languages in Coq. - Christian Doczkal; Jan-Oliver Kaiser; Gert Smolka (CPP, 2013)

Completeness and Decidability Results for CTL in Coq. - Christian Doczkal; Gert Smolka (ITP, 2014)

Transfinite Constructions in Classical Type Theory. - Gert Smolka; Steven Schäfer; Christian Doczkal (ITP, 2015)

Two-Way Automata in Coq. - Christian Doczkal; Gert Smolka (ITP, 2016)

Completeness and Decidability Results for CTL in Constructive Type Theory. - Christian Doczkal; Gert Smolka (J. Autom. Reason., 2016)

A machine-checked constructive metatheory of computation tree logic. - Christian Doczkal (2016)

Completeness and decidability of converse PDL in the constructive type theory of Coq. - Christian Doczkal; Joachim Bard (CPP, 2018)

A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. - Christian Doczkal; Guillaume Combette; Damien Pous (ITP, 2018)

Treewidth-Two Graphs as a Free Algebra. - Christian Doczkal; Damien Pous (MFCS, 2018)

Regular Language Representations in the Constructive Type Theory of Coq. - Christian Doczkal; Gert Smolka (J. Autom. Reason., 2018)

Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. - Christian Doczkal; Damien Pous (CPP, 2020)

Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. - Christian Doczkal; Damien Pous (J. Autom. Reason., 2020)

A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. - Christian Doczkal (ITP, 2021)

Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. - Manuel Barbosa; Gilles Barthe; Christian Doczkal; Jelle Don; Serge Fehr; Benjamin Grégoire; Yu-Hsuan Huang; Andreas Hülsing; Yi Lee; Xiaodi Wu 001 (IACR Cryptol. ePrint Arch., 2023)

CV2EC: Getting the Best of Both Worlds. - Bruno Blanchet; Pierre Boutry; Christian Doczkal; Benjamin Grégoire; Pierre-Yves Strub (CSF, 2024)