I am a former member of the Theorem Proving Group at TUM, headed by Tobias Nipkow, working on the Isabelle theorem prover. In my dissertation I developed a defininition mechanism for recursive functions, and methods to prove termination of such functions automatically.
I left TUM in August 2011, and now work as a Principal Software Architect at QAware GmbH, designing and building business software for corporate customers.
Currently (April - September 2019), I am spending a research sabbatical at TUM. I am working to develop a soft type system on top of a set-theoretic logic.