Philipp G. Haselwarter

23 papers A 1B 1Journal 19Unranked 2
YearRankTypeTitle / Venue / Authors
2025 J jnl
Approximate Relational Reasoning for Higher-Order Probabilistic Programs.
Proc. ACM Program. Lang.
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.
CoRR
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.
Proc. ACM Program. Lang.
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Almost-Sure Termination by Guarded Refinement.
CoRR
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Almost-Sure Termination by Guarded Refinement.
Proc. ACM Program. Lang.
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Approximate Relational Reasoning for Higher-Order Probabilistic Programs.
CoRR
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
Proc. ACM Program. Lang.
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
CoRR
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
Proc. ACM Program. Lang.
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
CoRR
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
Proc. ACM Program. Lang.
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2024 B conf
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
CPP
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
2023 J jnl
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
CoRR
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2023 J jnl
Finitary Type Theories With and Without Contexts.
J. Autom. Reason.
Philipp G. Haselwarter, Andrej Bauer
2023 J jnl
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
ACM Trans. Program. Lang. Syst.
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
2023 J jnl
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
IACR Cryptol. ePrint Arch.
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
2021 J jnl
Finitary type theories with and without contexts.
CoRR
Philipp G. Haselwarter, Andrej Bauer
2021 A conf
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
CSF
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
2021 J jnl
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
IACR Cryptol. ePrint Arch.
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
2020 J jnl
A general definition of dependent type theories.
CoRR
Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine
2020 — conf
Equality Checking for General Type Theories in Andromeda 2.
ICMS
Andrej Bauer, Philipp G. Haselwarter, Anja Petkovic
2018 J jnl
Design and Implementation of the Andromeda Proof Assistant.
CoRR
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone
2016 — conf
Design and Implementation of the Andromeda Proof Assistant.
TYPES
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone