Post-doc, member of the CoVeCe Project
ENS de Lyon)
I obtained my PhD at Saarland University in 2016 under the supervision of Gert Smolka.
My research is mainly focused on the formalization of mathematics in the constructive type theory of the proof assistant Coq.
I have developed formal machine-checked theories for a variety of topics including meta theory of modal logics, automata theory, set theory, and graph theory.
- Christian Doczkal and Damien Pous, Treewidth-Two Graphs as a Free Algebra (accepted for publication in MFCS 2018)
- 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
- 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
- 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, Los Angeles, USA, January 8-9, 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
|Email:||christian.doczkal at ens-lyon dot fr
|Office:|| GN1 Nord 3 70, LIP, ENS Lyon