Christian Doczkal

Postdoc researcher, Max Planck Institute for Security and Privacy (MPI-SP)

About Me

I obtained my PhD at Saarland University in 2016 under the supervision of Gert Smolka. From 2016 to 2019, I was a postdoc at the ENS Lyon as part of the ERC CoVeCe Project of Damien Pous. From 2019 to 2021, I was a postdoc in the STAMP team at Inria Sophia Antipolis Méditerranée with an individual young researcher grant from UCA-JEDI From 2021 to 2023, I worked at the MPI-SP in Bochum.

My research is mainly focused on the formalization of mathematics. In the past, I have worked mostly in the constructive type theory of the proof assistant Coq, developing formal machine-checked theories for a variety of topics including metatheory of modal logics, automata theory, set theory, and graph theory.

In the last two years, I have been working on cryptographic proofs in EasyCrypt. In particular, I contributed to the mechanization of the security proof of Dilithium, a Round 3 candidate for the NIST post-quantum cryptography project.

I have been working on building a graph library for Coq, which is available here.

Publications (2016 and later)

• Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, and Pierre-Yves Strub. CV2EC: Getting the Best of Both Worlds Computer Security Foundations Symposium (CSF 2024) (accepted for publication) [PDF]
• Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, and Xiaodi Wu, Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium CRYPTO (5) 2023: 358-389. [PDF]
• Christian Doczkal, A Variant of Wagner's Theorem Based on Combinatorial Hypermaps Interactive Theorem Proving (ITP 2021), LIPIcs vol 193, 2021. [PDF]
• Christian Doczkal and Damien Pous, Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020. [PDF] [Coq]
• Christian Doczkal and Damien Pous, Graph Theory in Coq: Minors, Treewidth, and Isomorphisms, Journal of Automated Reasoning (special issue for ITP 2018), Springer, 2020. [PDF] [Coq] [authorizer link]
• Christian Doczkal and Damien Pous, Treewidth-Two Graphs as a Free Algebra, Mathematical Foundations of Computer Science (MFCS 2018), LIPIcs vol. 117, Schloss Dagstuhl, 2018 [PDF]
• Christian Doczkal, Guillaume Combette, and Damien Pous, A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs, Interactive Theorem Proving (ITP 2018), LNCS vol. 10895, Springer, 2018 [PDF] [Coq]
• Christian Doczkal and Gert Smolka, Regular Language Representations in the Constructive Type Theory of Coq, Journal of Automated Reasoning (special issue on Milestones in Interactive Theorem Proving), Springer, 2018 [PDF] [Coq] [authorizer link]
• Christian Doczkal and Joachim Bard, Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), ACM, 2018 [PDF] [Coq]
• Christian Doczkal, A Machine-Checked Constructive Metatheory of Computation Tree Logic, PhD Thesis, Saarland University, 2016 [UdS]

For a complete list of publications see DBLP. Publications from my time at Saarland University can be obtained from the Programming Systems Lab

Coordinates