Philipp G. Haselwarter

Publication Activity (10 Years)

Years Active: 2016-2024
Publications (10 Years): 17

Top Topics

Container Terminal

Probabilistic Reasoning

Top Venues

IACR Cryptol. ePrint Arch.

Proc. ACM Program. Lang.

Publications

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