I am a postdoc at Aarhus University working with Lars Birkedal. Before this, I was a PhD student at the Imdea Software Institute in Madrid under the supervision of Gilles Barthe.
Email : [first name][at]cs[dot]au[dot]dk
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.POPL '24
Alejandro Aguirre, Lars Birkedal.
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice.POPL '23
Alejandro Aguirre, Shin-ya Katsumata, Satoshi Kura.
Weakest Preconditions in Fibrations (Journal Version).MSCS
Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe.
Symbolic Synthesis of Indifferentiability Attacks.ASIA CCS '22
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato.
Higher-order probabilistic adversarial computations: categorical semantics and program logics.ICFP '21
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.
A Pre-Expectation Calculus for Probabilistic Sensitivity.
POPL '21 (Distinguished Paper Award)
Alejandro Aguirre, Shin-ya Katsumata.
Weakest Preconditions in Fibrations
MFPS 2020
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
A relational logic for higher-order programs (Journal Version). JFP
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
Formal Verification of Higher-Order Probabilistic Programs. POPL '19
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva.
Almost Sure Productivity. ICALP '18
[ArXiV extended version]
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg.
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. ESOP '18
[Slides]
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
A relational logic for higher-order programs. ICFP '17
[Slides]
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Almost-Sure Termination by Guarded Refinement. Submitted
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. Submitted
2016-2021 PhD in Computer Science.
Universidad Politécnica de Madrid, Madrid, Spain
2015-2016 Masters of Research in Informatics.
Université Paris 7, Paris, France
2010-2015 Double Degree in Mathematics and Computer Science.
Universidad Complutense de Madrid, Madrid, Spain