Welcome

My name is Philipp Haselwarter, I'm a second-year doctoral student of at the faculty of mathematics of the University of Ljubljana. My supervisor is Andrej Bauer. Currently, I am working on Andromeda, an open source implementation of type theory with equality reflection inspired by Martin-Löf's 1982 Constructive mathematics and computer programming. Unlike traditional proof assistants, our meta-language is based on computational effects and handlers.

I hold a masters degree in theoretical computer science (MPRI). Most of 2014, I spent interning under the supervision of Matthieu Sozeau in the πr² team at PPS, where I worked on a version of the (predicative) Calculus of Constructions internalizing proof irrelevance.
This lead to my master's thesis, which I defended on the 3rd of September 2014 (slides of the defense).

During my first year of masters, I worked on grammatical inference for finite memory automata under Peter Habermehl. Before that I did obtained a Licence (french bachelors) in computer science and applied mathematics from Université Piere et Marie Curie (Paris 6).

Nowadays my centers of interest are logic and type theory, in particular the homotopical variant, theorem provers and programming languages. Apart from that my time goes into yoga, dance, rock climbing and cycling.

tl;dr : here's my cv.

In case you happen not to be in Ljubljana , you can send me an email to philipp at haselwarter dot org or ph at pps.univ-paris-diderot.fr. For urgent matters, you can find my phone number on my CV.

people: Thibaut Girka, Jakob Vidmar, Kenji Maillard, Luc Pellissier, Raphaël Proust