Assistant Professor
Aarhus University
Office: Turing-228
philipp at haselwarter . org

————————————————————————————————————

About me

I am member of the Logic and Semantics group at Aarhus University. I am interested in programming languages, type theory, and mechanised proofs. Currently, I work with Lars Birkedal on program logics for probabilistic programming languages.

Previously, with Bas Spitters I applied language design and type theory to cryptography at Aarhus University's Concordium Blockchain Research Centre Aarhus (COBRA). During my PhD with Andrej Bauer, I developed 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

• Approximate Relational Reasoning for Higher-Order Probabilistic Programs.
  Under submission.
  P. G. Haselwarter, K. H. Li, A. Aguirre, S. O. Gregersen, J. Tassarotti, and L. Birkedal.
• A general definition of dependent type theories.
  Under revision.
  Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine.
• The Andromeda Metalanguage.
  Forthcoming, see chapter 4 of my PhD thesis.
  
  

Publications

• Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
  OOPSLA'24.
  P. G. Haselwarter, K. H. Li, M. de Medeiros, S. O. Gregersen, A. Aguirre, J. Tassarotti, and L. Birkedal.
• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
  ICFP'24; distinguished paper award.
  A. Aguirre, P. G. Haselwarter, M. de Medeiros, K. H. Li, S. O. Gregersen, J. Tassarotti, and L. Birkedal. (arxiv: long version)
• Almost-Sure Termination by Guarded Refinement.
  ICFP'24.
  S. O. Gregersen, A. Aguirre, P. G. Haselwarter, J. Tassarotti, and L. Birkedal. (arxiv: long version)
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
  POPL’24.
  Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal. (arxiv: long version)
• The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
  CPP’24.
  Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hrițcu, Bas Spitters. (eprint archive, formalisation)
• Finitary type theories, with and without contexts.
  Journal of Automated Reasoning.
  Philipp G. Haselwarter, Andrej Bauer. (arxiv preprint)
• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq (Journal version).
  ACM Transactions on Programming Languages and Systems (TOPLAS).
  Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Cătălin Hrițcu, Kenji Maillard, Bas Spitters. (eprint archive, formalisation)
• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
  2021 IEEE 34th Computer Security Foundations Symposium (CSF); distinguished paper award.
  Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Cătălin Hrițcu, Kenji Maillard, Bas Spitters. (eprint archive, formalisation)
• Type theories without contexts.
  TYPES’21 extended abstract.
  Andrej Bauer and Philipp G. Haselwarter.
• Equality Checking for General Type Theories in Andromeda 2.
  International Congress on Mathematical Software (ICMS) 2020.
  Andrej Bauer, Philipp G. Haselwarter, Anja Petković.
• Finitary general type theories in computational form.
  TYPES’20 extended abstract.
  Andrej Bauer and Philipp G. Haselwarter.
• On equality checking for general type theories: Implementation in Andromeda 2.
  TYPES’20 extended abstract.
  Andrej Bauer, Philipp G. Haselwarter, and Anja Petković.
• A modular formalization of type theory in Coq.
  TYPES’17 extended abstract.
  Andrej Bauer, Philipp G. Haselwarter, Théo Winterhalter.
• Design and Implementation of the Andromeda Proof Assistant.
  TYPES’16 postproceedings.
  Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone.
  
  

Thesis

Effective Metatheory for Type Theory.
PhD thesis, Faculty of Mathematics and Physics, University of Ljubljana. (university archive)
Committee: Andrej Bauer, Robert Harper, Matija Pretnar, Tomaž Košir.

Software

• Andromeda is an implementation of finitary type theories, allowing the user to define their own type theory. It features an ML style metalanguage that supports proof development via runners and bidirectional evaluation.
• Clutch is a higher-order probabilistic relational separation logic with support for asynchronous probabilistic couplings. Clutch is based on the Iris logic, and embedded in the Coq interactive prover.
• SSProve is a formalisation of a relational program logic for reasoning about cryptographic code. It supports packages in the sense of state-separating proofs, enabling modular proofs of program equivalence.

Selected talks

• Tachis: Higher-Order Separation Logic with Credits for Expected Costs (slides).
  Iris Workshop. Zurich, 04.06.2024.
• Effective Metatheory for Type Theory (slides).
  Slides from the defence of my PhD thesis. Ljubljana, 11.01.2022.
• Type theories without contexts.
  Slides accompanying the video recording (timestamp: 46:35) presented at TYPES’21.
• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
  Slides accompanying the video recording presented at CSF’21.
• 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.