Design and Implementation of the Andromeda Proof Assistant. - Andrej Bauer; Gaëtan Gilbert; Philipp G. Haselwarter; Matija Pretnar; Christopher A. Stone (TYPES, 2016)

Equality Checking for General Type Theories in Andromeda 2. - Andrej Bauer; Philipp G. Haselwarter; Anja Petkovic (ICMS, 2020)

A general definition of dependent type theories. - Andrej Bauer; Philipp G. Haselwarter; Peter LeFanu Lumsdaine (CoRR, 2020)

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 (IACR Cryptol. ePrint Arch., 2021)

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 (IACR Cryptol. ePrint Arch., 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., 2023)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2023)

Finitary Type Theories With and Without Contexts. - Philipp G. Haselwarter; Andrej Bauer (J. Autom. Reason., 2023)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Almost-Sure Termination by Guarded Refinement. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 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 001; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs - Coq Artifact. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Almost-Sure Termination by Guarded Refinement - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs - Formalization Artifact. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. - Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (CoRR, 2025)