This web page is about my research in **Mathematical Logic**
and **Computer Science** on using perls from the theory of
programming languages (continuations,
partial
evaluation, type
isomorphisms) in order to interpret logical principles such as
the axiom of
choice or completeness
theorems; I have also done quite a bit of formal proof
development using proof assistants such as Coq.

I work at Siemens Mobility on verification of software for driverless trains. Previously, I was a formal methods expert at Trusted Labs where I was involved in Common Criteria evaluations. The preceding 9 years, I was doing research and teaching -- I still try to keep up with academic research.

Publications | Formal Proofs and Software | Teaching | CV | Contact

*(September 2018)*1 PhD student position in formal methods under my supervision; apply here*(August 2018)*The paper An Intuitionistic Formula Hierarchy Based on High-School Identities (**with Taus Brock-Nannestad**) to appear in Mathematical Logic Quarterly*(January 2018)*Talk at EUTypes 2018 Working Meeting in Nijmegen, The Netherlands*(December 2017)*My Perspectives for proof unwinding by programming languages techniques was published in IfColog Journal of Logics and their Applications, volume 4 (10), 2017*(February 2017)*Talk at CHoCoLa, ENS Lyon*(January 2017)*Talk at 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) on The exp-log normal form of types