Alejandro Aguirre

34 papers A* 1A 2B 2Journal 28
YearRankTypeTitle / Venue / Authors
2026 B conf
Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic.
CPP
Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal
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
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs.
CoRR
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Modelling Recursion and Probabilistic Choice in Guarded Type Theory.
Proc. ACM Program. Lang.
Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, 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
Modelling Probabilistic FPC in Guarded Type Theory.
CoRR
Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, 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
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
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice.
Proc. ACM Program. Lang.
Alejandro Aguirre, Lars Birkedal
2022 A conf
Symbolic Synthesis of Indifferentiability Attacks.
AsiaCCS
Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe
2022 J jnl
Weakest preconditions in fibrations.
Math. Struct. Comput. Sci.
Alejandro Aguirre, Shin-ya Katsumata, Satoshi Kura
2021 J jnl
A pre-expectation calculus for probabilistic sensitivity.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2021 J jnl
Higher-order probabilistic adversarial computations: Categorical semantics and program logics.
CoRR
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato
2021 J jnl
Higher-order probabilistic adversarial computations: categorical semantics and program logics.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato
2020 — —
Relational logics for higher-order effectful programs.
Alejandro Aguirre
2020 B conf
Weakest Preconditions in Fibrations.
MFPS
Alejandro Aguirre, Shin-ya Katsumata
2019 J jnl
A relational logic for higher-order programs.
J. Funct. Program.
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
2019 J jnl
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.
Proc. ACM Program. Lang.
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu
2019 J jnl
Kantorovich Continuity of Probabilistic Programs.
CoRR
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2018 A* conf
Almost Sure Productivity.
ICALP
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva
2018 J jnl
Almost Sure Productivity.
CoRR
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva
2018 J jnl
Formal verification of higher-order probabilistic programs.
CoRR
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu
2018 A conf
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.
ESOP
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
2018 J jnl
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.
CoRR
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
2017 J jnl
A Relational Logic for Higher-Order Programs.
CoRR
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
2017 J jnl
A relational logic for higher-order programs.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub