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)

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

Coordinates

Email: christian.doczkal at mpi-sp dot org