Philipp G. Haselwarter

I am an Assistant Professor in the Programming Languages, Logic, and Software Security section at Aarhus University. My research spans programming languages, type theory, and formal verification. A central theme is the development of machine-checked logical foundations for probabilistic programs, with applications to security and privacy.

I am one of the main developers of Clutch, a family of higher-order probabilistic separation logics formalised in Rocq, covering properties such as differential privacy, expected resource bounds, and relational reasoning about randomised programs. Earlier I worked on machine-checked cryptographic proofs (SSProve) and on the foundations and implementation of general type theories (Andromeda).

News

Publications

Papers

Preprints

Dissertation

Software

• Andromeda — 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 — 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 — 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