Christian Doczkal

According to our database, Christian Doczkal authored at least 19 papers between 2009 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

CV2EC: Getting the Best of Both Worlds.

Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub

Proceedings of the 37th IEEE Computer Security Foundations Symposium, 2024

2023

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

IACR Cryptol. ePrint Arch., 2023

2021

A Variant of Wagner's Theorem Based on Combinatorial Hypermaps.

Christian Doczkal

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020

Graph Theory in Coq: Minors, Treewidth, and Isomorphisms.

Christian Doczkal, Damien Pous

J. Autom. Reason., 2020

Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq.

Christian Doczkal, Damien Pous

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2018

Regular Language Representations in the Constructive Type Theory of Coq.

Christian Doczkal, Gert Smolka

J. Autom. Reason., 2018

Treewidth-Two Graphs as a Free Algebra.

Christian Doczkal, Damien Pous

Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science, 2018

A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs.

Christian Doczkal, Guillaume Combette, Damien Pous

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Completeness and decidability of converse PDL in the constructive type theory of Coq.

Christian Doczkal, Joachim Bard

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2016

A machine-checked constructive metatheory of computation tree logic.

Christian Doczkal

PhD thesis, 2016

Completeness and Decidability Results for CTL in Constructive Type Theory.

Christian Doczkal, Gert Smolka

J. Autom. Reason., 2016

Two-Way Automata in Coq.

Christian Doczkal, Gert Smolka

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2015

Transfinite Constructions in Classical Type Theory.

Gert Smolka, Steven Schäfer, Christian Doczkal

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

Completeness and Decidability Results for CTL in Coq.

Christian Doczkal, Gert Smolka

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

A Constructive Theory of Regular Languages in Coq.

Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

Constructive Completeness for Modal Logic with Transitive Closure.

Christian Doczkal, Gert Smolka

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Constructive Formalization of Hybrid Logic with Eventualities.

Christian Doczkal, Gert Smolka

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Strong Normalization of Moggis's Computational Metalanguage.

Christian Doczkal

Arch. Formal Proofs, 2010

2009

Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal.

Christian Doczkal, Jan Schwinghammer

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2009