Philipp G. Haselwarter

According to our database, Philipp G. Haselwarter authored at least 21 papers between 2016 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version).

Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal

CoRR, April, 2026

2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Gregesen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Gregesen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Gregesen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, May, 2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2025

Approximate Relational Reasoning for Higher-Order Probabilistic Programs.

Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2025

2024

Approximate Relational Reasoning for Higher-Order Probabilistic Programs - Formalization Artifact.

Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Dataset, October, 2024

Almost-Sure Termination by Guarded Refinement - Coq Artifact.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2024

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs - Coq Artifact.

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2024

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., January, 2024

Tachis: Higher-Order Separation Logic with Credits for Expected Costs.

Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2024

Almost-Sure Termination by Guarded Refinement.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2024

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2024

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.

Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Finitary Type Theories With and Without Contexts.

Philipp G. Haselwarter, Andrej Bauer

J. Autom. Reason., December, 2023

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, October, 2023

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.

Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters

ACM Trans. Program. Lang. Syst., September, 2023

2021

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.

Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

A general definition of dependent type theories.

Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine

CoRR, 2020

Equality Checking for General Type Theories in Andromeda 2.

Andrej Bauer, Philipp G. Haselwarter, Anja Petkovic

Proceedings of the Mathematical Software - ICMS 2020, 2020

2016

Design and Implementation of the Andromeda Proof Assistant.

Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016