A relational logic for higher-order programs. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Pierre-Yves Strub (Proc. ACM Program. Lang., 2017)

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. - Alejandro Aguirre 001; Gilles Barthe; Lars Birkedal; Ales Bizjak; Marco Gaboardi; Deepak Garg 001 (ESOP, 2018)

Almost Sure Productivity. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Alexandra Silva 001 (ICALP, 2018)

Formal verification of higher-order probabilistic programs. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (CoRR, 2018)

Kantorovich Continuity of Probabilistic Programs. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (CoRR, 2019)

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (Proc. ACM Program. Lang., 2019)

Weakest Preconditions in Fibrations. - Alejandro Aguirre 001; Shin-ya Katsumata (MFPS, 2020)

Relational logics for higher-order effectful programs. - Alejandro Aguirre 001 (2020)

A pre-expectation calculus for probabilistic sensitivity. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2021)

Higher-order probabilistic adversarial computations: categorical semantics and program logics. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Shin-ya Katsumata; Tetsuya Sato 001 (Proc. ACM Program. Lang., 2021)

Symbolic Synthesis of Indifferentiability Attacks. - Itsaka Rakotonirina; Miguel Ambrona; Alejandro Aguirre 001; Gilles Barthe (AsiaCCS, 2022)

Weakest preconditions in fibrations. - Alejandro Aguirre 001; Shin-ya Katsumata; Satoshi Kura 001 (Math. Struct. Comput. Sci., 2022)

Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. - Alejandro Aguirre 001; Lars Birkedal (Proc. ACM Program. Lang., 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)

Modelling Probabilistic FPC in Guarded Type Theory. - Philipp Stassen; Rasmus Ejlers Møgelberg; Maaike Zwart; Alejandro Aguirre 001; Lars Birkedal (CoRR, 2024)

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)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory. - Philipp Stassen; Rasmus Ejlers Møgelberg; Maaike Zwart; Alejandro Aguirre 001; 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)