Completeness and decidability of converse PDL in the constructive type theory of Coq
(pdf)
Christian Doczkal, Joachim Bard
7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, USA, January 8-9, 2018
Regular Language Representations in the Constructive Type Theory of Coq
(pdf)
Christian Doczkal, Gert Smolka
Journal of Automated Reasoning
Two-Way Automata in Coq
(pdf)
Christian Doczkal, Gert Smolka
Interactive Theorem Proving (ITP 2016)
A Machine-Checked Constructive Metatheory of Computation Tree Logic
(pdf)
Christian Doczkal
PhD Thesis, Saarland University
Completeness and Decidability Results for CTL in Constructive Type Theory
(pdf)
Christian Doczkal, Gert Smolka
Journal of Automated Reasoning
Transfinite Constructions in Classical Type Theory
(pdf)
Gert Smolka, Steven Schäfer, Christian Doczkal
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015
Completeness and Decidability Results for CTL in Coq
(pdf)
Christian Doczkal, Gert Smolka
Interactive Theorem Proving (ITP 2014)
A Constructive Theory of Regular Languages in Coq
(pdf)
Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka
Certified Programs and Proofs, Third International Conference (CPP 2013)
Constructive Completeness for Modal Logic with Transitive Closure
(pdf)
Christian Doczkal, Gert Smolka
Certified Programs and Proofs, Second International Conference (CPP 2012)
Constructive Formalization of Hybrid Logic with Eventualities
(pdf)
Christian Doczkal, Gert Smolka
Certified Programs and Proofs, First International Conference (CPP 2011)
Formalizing TT-lifting in Isabelle/HOL-Nominal
(pdf)
Christian Doczkal
Master's Thesis, Saarland University
Formalizing a Strong Normalization Proof for Moggi's Computational Metalanguage
(pdf)
Christian Doczkal, Jan Schwinghammer
4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'09)
A Proof of Strong Normalization for Call-by-push-value
(pdf)
Christian Doczkal, Jan Schwinghammer
Strong Normalization of Call-by-push-value
(pdf)
Christian Doczkal
B.Sc. Thesis, Programming Systems Lab, Department of Informatics, Saarland University