philipp at haselwarter . org
My name is Philipp Haselwarter, I’m a postdoctoral fellow in the LogSem group at Aarhus University, and doctoral student at the faculty of mathematics in Ljubljana (thesis under review). My advisor is Andrej Bauer. I study the interplay of type theory, proof assistants, and programming languages. With Bas Spitters I apply language design and type theory to cryptography. During my PhD, I have been developing the Andromeda prover, a proof assistant that lets the user define their own type theory, and write programs proving theorems in a meta language based on algebraic effects and handlers à la Eff.
This site is under construction
- A general definition of dependent type theories, with Andrej Bauer and Peter LeFanu Lumsdaine
- Andromeda 2.0
- An Effective Metatheory for Type Theory (PhD thesis) – currently under review
- Andromeda TYPES’16