Formosa Crypto | The Formosa project federates multiple projects in machine-checked cryptography and high-assurance cryptographi
Description: Christian Doczkal's Professional webpage
christian doczkal; computer science; modal logic; regular langua (1) christian doczkal; computer science; modal logic; regular langua
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 Currently, I am at 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. Recently, I have started doing cryptographic proofs in EasyCrypt.
I have been working on building a graph library for Coq, which is available here .
Formosa Crypto | The Formosa project federates multiple projects in machine-checked cryptography and high-assurance cryptographi