Martin Riener

My former positions include the Theory and Logic Group at the Technical University of Vienna where I had the pleasure of writing my PhD thesis on applications of higher-order cut-elimination via automated theorem provers. I am still involved in the development of the GAPT framework and use it for my experiments.

I also enjoyed being part of the VeriDis team at INRIA Nancy where I worked on TLAPS, an interactive proof system for the first-order temporal logic TLA+.

After that I had the pleasure of joining the team of Giles Reger at the University of Manchester to work on theory reasoning for the Vampire theorem prover.