Christian Doczkal

20 papers A 1B 11Journal 5Unranked 2
YearRankTypeTitle / Venue / Authors
2024 A conf
CV2EC: Getting the Best of Both Worlds.
CSF
Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub
2023 — conf
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium.
CRYPTO (5)
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
2023 J jnl
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
2021 B conf
A Variant of Wagner's Theorem Based on Combinatorial Hypermaps.
ITP
Christian Doczkal
2020 B conf
Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq.
CPP
Christian Doczkal, Damien Pous
2020 J jnl
Graph Theory in Coq: Minors, Treewidth, and Isomorphisms.
J. Autom. Reason.
Christian Doczkal, Damien Pous
2018 B conf
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs.
ITP
Christian Doczkal, Guillaume Combette, Damien Pous
2018 B conf
Completeness and decidability of converse PDL in the constructive type theory of Coq.
CPP
Christian Doczkal, Joachim Bard
2018 J jnl
Regular Language Representations in the Constructive Type Theory of Coq.
J. Autom. Reason.
Christian Doczkal, Gert Smolka
2018 B conf
Treewidth-Two Graphs as a Free Algebra.
MFCS
Christian Doczkal, Damien Pous
2016 — —
A machine-checked constructive metatheory of computation tree logic.
Christian Doczkal
2016 J jnl
Completeness and Decidability Results for CTL in Constructive Type Theory.
J. Autom. Reason.
Christian Doczkal, Gert Smolka
2016 B conf
Two-Way Automata in Coq.
ITP
Christian Doczkal, Gert Smolka
2015 B conf
Transfinite Constructions in Classical Type Theory.
ITP
Gert Smolka, Steven Schäfer, Christian Doczkal
2014 B conf
Completeness and Decidability Results for CTL in Coq.
ITP
Christian Doczkal, Gert Smolka
2013 B conf
A Constructive Theory of Regular Languages in Coq.
CPP
Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka
2012 B conf
Constructive Completeness for Modal Logic with Transitive Closure.
CPP
Christian Doczkal, Gert Smolka
2011 B conf
Constructive Formalization of Hybrid Logic with Eventualities.
CPP
Christian Doczkal, Gert Smolka
2010 J jnl
Strong Normalization of Moggis's Computational Metalanguage.
Arch. Formal Proofs
Christian Doczkal
2009 — conf
Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal.
LFMTP
Christian Doczkal, Jan Schwinghammer