Logic, Interactive Theorem Proving, Automated Reasoning, Functional Programming
Interests:
 SMTsolving (e.g. conflictdriven satisfiability)
 Combination of logicbased AI and machine learning, AI safety
(e.g. verification of neural nets, learning for proofsearch guidance)
 Type systems, type theory, models of proofs and programs (e.g. realisability)
 Correctbyconstruction software, formal specifications within software development

