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

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

About me

I am a postdoctoral researcher in the Logic and Semantics group at Aarhus University. I am interested in progamming languages, type theory, and mechanised proofs. Currently, I work with Lars Birkedal on reasoning for and verification of probabilistic programs. With Bas Spitters I applied language design and type theory to cryptography at the Concordium Blockchain Research Centre Aarhus (COBRA). During my PhD with Andrej Bauer, I developped 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

• The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
  Submitted.
  Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters. (formalisation)
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
  Submitted.
  Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal.
• A general definition of dependent type theories.
  Under revision.
  Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine.
• Finitary type theories, with and without contexts. Under revision.
  Philipp G. Haselwarter, Andrej Bauer.
• The Andromeda Metalanguage.
  Forthcoming, see chapter 4 of my thesis.
  
  

Publications

• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq (Journal version). 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

• 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.
• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
  Logic & Semantics seminar Aarhus, March 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.