Dr Théo Winterhalter
Formally Verified Security
Personal website | DBLP | Google Scholar
Théo Winterhalter is post-doc working with Cătălin Hrițcu on applying formal methods to security, in particular methods pertaining to dependent types and type theory.
He concluded a three-year PhD with Nicolas Tabareau and Matthieu Sozeau at the University of Nantes (France), working on formalisation and meta-theory of type theory. As part of his PhD thesis, he contributed to the MetaCoq project which allows for meta-programming in Coq, as well as reasoning about the meta-theory and implementation of Coq itself.