Postdoctoral Research Fellow
Aarhus University
Office: Nygaard-391
philipp at haselwarter . org
——————————————————————————————————
About me
My name is Philipp Haselwarter, I’m a postdoctoral fellow in the Logic and Semantics group at Aarhus University, and PhD candidate at the Faculty of Mathematics and Physics in Ljubljana (thesis under review). My PhD 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 at the Concordium Blockchain Research Centre Aarhus (COBRA). 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.
Preprints
- SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq, Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Cătălin Hrițcu, Kenji Maillard, Bas Spitters. (CSF talk recording)
- A general definition of dependent type theories, Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine.
- An Effective Metatheory for Type Theory (PhD thesis) – currently under review
- Finitary type theories, with and without contexts – awaiting thesis review
- Andromeda 2.0 – awaiting thesis review
Publications
- Equality Checking for General Type Theories in Andromeda 2, ICMS 2020. Andrej Bauer, Philipp G. Haselwarter, Anja Petković.
- A modular formalization of type theory in Coq (extended abstract), TYPES’17. Andrej Bauer, Philipp G. Haselwarter, Théo Winterhalter.
- Design and Implementation of the Andromeda Proof Assistant, TYPES’16. Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone.
Talks
- SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq, Logic & Semantics seminar Aarhus, 2021.
- Computer Formalisation of Mathematics, Meeting of young mathematicians in Slovenia, 2019.
- A general definition of dependent type theories, Logic & Semantics seminar Aarhus, 2019.
- Andromeda 2.0, Foundations Seminar, Faculty of Mathematics and Physics Ljubljana, 2018.
- Algorithmic Inversion Principles in Extensional Type Theory, EUTypes Nijmegen, 2018.
- Design and Implementation of Andromeda, TYPES’16, 2016.