Alejandro Aguirre

According to our database, Alejandro Aguirre authored at least 33 papers between 2018 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic.

Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti

CoRR, May, 2026

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version).

Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal

CoRR, April, 2026

Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic.

Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026

2025

Artifact for Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic.

Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal

Dataset, December, 2025

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal

CoRR, November, 2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Gregesen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Gregesen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Gregesen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, May, 2025

Modelling Recursion and Probabilistic Choice in Guarded Type Theory.

Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal

Proc. ACM Program. Lang., 2025

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.

Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2025

Approximate Relational Reasoning for Higher-Order Probabilistic Programs.

Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2025

2024

Approximate Relational Reasoning for Higher-Order Probabilistic Programs - Formalization Artifact.

Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Dataset, October, 2024

Almost-Sure Termination by Guarded Refinement - Coq Artifact.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2024

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs - Coq Artifact.

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Dataset, June, 2024

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., January, 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, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2024

Almost-Sure Termination by Guarded Refinement.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2024

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.

Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal

Proc. ACM Program. Lang., 2024

Modelling Probabilistic FPC in Guarded Type Theory.

Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal

CoRR, 2024

2023

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact.

Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal

Dataset, October, 2023

Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice.

Alejandro Aguirre, Lars Birkedal

Proc. ACM Program. Lang., January, 2023

2022

Weakest preconditions in fibrations.

Alejandro Aguirre, Shin-ya Katsumata, Satoshi Kura

Math. Struct. Comput. Sci., April, 2022

Symbolic Synthesis of Indifferentiability Attacks.

Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe

Proceedings of the ASIA CCS '22: ACM Asia Conference on Computer and Communications Security, Nagasaki, Japan, 30 May 2022, 2022

2021

Higher-order probabilistic adversarial computations: categorical semantics and program logics.

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato

Proc. ACM Program. Lang., 2021

A pre-expectation calculus for probabilistic sensitivity.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Proc. ACM Program. Lang., 2021

2020

Relational logics for higher-order effectful programs.

Alejandro Aguirre

PhD thesis, 2020

Weakest Preconditions in Fibrations.

Alejandro Aguirre, Shin-ya Katsumata

Proceedings of the 36th Conference on the Mathematical Foundations of Programming Semantics, 2020

2019

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.

Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu

Proc. ACM Program. Lang., 2019

A relational logic for higher-order programs.

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub

J. Funct. Program., 2019

Kantorovich Continuity of Probabilistic Programs.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

CoRR, 2019

2018

Formal verification of higher-order probabilistic programs.

Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu

CoRR, 2018

Almost Sure Productivity.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva

Proceedings of the 45th International Colloquium on Automata, Languages, and Programming, 2018

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.

Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg

Proceedings of the Programming Languages and Systems, 2018