Postdoctoral Fellow
Aarhus University
Office: Nygaard-391
philipp at haselwarter . org

---

Welcome

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, with Andrej Bauer and Peter LeFanu Lumsdaine
• Andromeda 2.0
• An Effective Metatheory for Type Theory (PhD thesis) – currently under review

Publications

• Andromeda TYPES’16
• …

Talks

• …