About me

I am a non-tenure track Assistant Professor at Aarhus University. Before this, I was a postdoc at Aarhus University, working with Lars Birkedal. I obtained my PhD from the Imdea Software Institute and the Technical University of Madrid under the supervision of Gilles Barthe.

Email : [first name][at]cs[dot]au[dot]dk

Research interests

Publications

  1. Virgil Marionneau, Félix Sassus-Bourda, Alejandro Aguirre, Lars Birkedal Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic. CPP '26

  2. Kwing Hei Li, Alejandro Aguirre, Simon Gregesen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. ICFP '25

  3. Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal Modelling Recursion and Probabilistic Choice in Guarded Type Theory. POPL '25

  4. Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
    Approximate Relational Reasoning for Higher-Order Probabilistic Programs. POPL '25

  5. Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
    Tachis: Higher-Order Separation Logic with Credits for Expected Costs. OOPSLA '24

  6. Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
    Almost-Sure Termination by Guarded Refinement. ICFP '24

  7. 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. ICFP '24
    Recipient of Distinguished Paper Award

  8. Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
    Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.POPL '24

  9. Alejandro Aguirre, Lars Birkedal.
    Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice.POPL '23

  10. Alejandro Aguirre, Shin-ya Katsumata, Satoshi Kura.
    Weakest Preconditions in Fibrations (Journal Version).MSCS

  11. Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe.
    Symbolic Synthesis of Indifferentiability Attacks.ASIA CCS '22

  12. 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

  13. Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.
    A Pre-Expectation Calculus for Probabilistic Sensitivity. POPL '21
    Recipient of Distinguished Paper Award

  14. Alejandro Aguirre, Shin-ya Katsumata.
    Weakest Preconditions in Fibrations MFPS 2020

  15. Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
    A relational logic for higher-order programs (Journal Version). JFP

  16. Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.
    Formal Verification of Higher-Order Probabilistic Programs. POPL '19

  17. Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva.
    Almost Sure Productivity. ICALP '18 [ArXiV extended version]

  18. 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]

  19. Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub.
    A relational logic for higher-order programs. ICFP '17 [Slides]

Pre-prints

  1. Philipp Georg Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic. Submitted

  2. Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal Contextual Refinement of Higher-Order Concurrent Probabilistic Programs. Submitted.

Education