Postdoctoral Fellow
Aarhus University
Office: Nygaard-391
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

Preprints

• A general definition of dependent type theories, Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine
• Andromeda 2.0
• An Effective Metatheory for Type Theory (PhD thesis) – currently under review

Publications

• Design and Implementation of the Andromeda Proof Assistant, TYPES’16, Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone
• …

Talks

• …