
معرفی
Alejandro Aguirre is a Research Fellow at Aarhus University, Department of Computer Science. Previously, he was a PhD student at Universidad Politécnica de Madrid and Imdea Software Institute under Gilles Barthe's supervision.
- Current Role: Postdoctoral Research Fellow at Aarhus University
- PhD Supervisors: Gilles Barthe, Lars Birkedal
- Education: PhD (2021), MRes (2016), Double Degree in Mathematics and Computer Science (2015)
His research focuses on Formal Verification, Probabilistic Programming, and Programming Language Semantics. He develops logical frameworks for verifying probabilistic and concurrent programs, including Separation Logic extensions, Guarded Type Theory, and Relational Reasoning. His work addresses challenges in probabilistic coupling, termination analysis, error bounds, and expected costs in higher-order programs.
The most recent articles highlight his contributions to asynchronous probabilistic couplings, error credits for resourceful reasoning, and guarded refinement for almost-sure termination. These works span Computer Science, Formal Methods, and Concurrency, with subfields like Program Logics, Probabilistic Reasoning, and Logical Relations.
Scientific Recognition:
- Distinguished Paper Award, ICFP '24
- Distinguished Paper Award, POPL '21
He has served on the Program Committee for POPL 2024 and OOPSLA Review Committee (SPLASH 2024). His work intersects Probabilistic Programming and Formal Verification, with applications to security, concurrency, and program logics.





