Written by Anna Klingenberg
Almost one month into his new role as Tenure-Track Assistant Professor, Alejandro Aguirre is looking ahead to the next stage of his career at the Department of Computer Science.
Alejandro joined Aarhus University in 2021 as a postdoc under the supervision of Professor Lars Birkedal. Before coming to Aarhus, he completed his bachelor's degree at Universidad Complutense de Madrid, earned his master's degree from Université Paris-Diderot in Paris, and later returned to Spain to complete a PhD at Universidad Politécnica de Madrid and IMDEA Software Institute.
Since arriving in Aarhus, Alejandro has established himself as a researcher in programming languages and program verification.
Alejandro's research focuses on the verification of probabilistic programs, a field concerned with proving that software behaves as intended, even when randomness is part of the computation.
"Probabilistic programs are used in many different areas, from privacy-preserving technologies to machine learning and cryptography," Alejandro explains. "My work is about developing mathematical techniques that allow us to verify that these systems actually behave as expected."
Much of his recent research has centered on differential privacy, a set of techniques designed to protect sensitive information while still allowing valuable insights to be extracted from data.
"When researchers design an algorithm on paper, they can often prove that it provides certain guarantees. What interests me is ensuring that those guarantees are still preserved once the algorithm is implemented and run as a real program."
In other words, his work helps bridge the gap between theory and practice, providing stronger confidence that privacy-preserving and security-critical software functions correctly in the real world.
One of the reasons Alejandro finds differential privacy particularly exciting is its potential societal impact.
The techniques make it possible to analyze large datasets, such as medical records or public statistics, while protecting the privacy of individual citizens. The goal is to allow researchers and organizations to learn from the data as a whole without the risk of personal information being exposed.
"You want to be able to use data in a meaningful way without compromising the privacy of the people behind it," he says.
As he begins his tenure-track position, Alejandro is interested in expanding the application of verification techniques to questions in security and cryptography. In particular, he hopes to strengthen connections between two different mathematical approaches to reasoning about secure systems: the symbolic model and the computational model. The symbolic model is easier to use and to scale to large systems, while the computational model is more realistic, but also harder to reason in. Bridging this gap will enable stronger guarantees for secure systems.
"It's a challenging problem, but I think we now have richer tools and languages for reasoning about these properties than we did before."
Aarhus University stood out to Alejandro, because of the collaboration opportunities with other researchers in his field.
"I knew the group here was doing research that closely matched my interests, and the project I joined seemed like a very good fit."
Five years later, he is still happy with the decision.
"There are many interesting people to collaborate with, many exciting projects, and Aarhus is also a very nice place to live."
When he is not working on programming languages and formal verification, Alejandro enjoys staying active. He is a regular climber at Aarhus Boulders and enjoys running. Music is another important hobby; he plays the guitar and is learning to play the piano.
A Pre-Expectation Calculus for Probabilistic Sensitivity
Aguirre, A., Barthe, G., Hsu, J., Kaminski, B. L., Katoen, J-P., Matheja, C.
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone function of the distance between the corresponding inputs. When programs are probabilistic, the distance between outputs is a distance between distributions. The Kantorovich lifting provides a general way of defining a distance between distributions by lifting the distance of the underlying sample space; by choosing an appropriate distance on the base space, one can recover other usual probabilistic distances, such as the Total Variation distance. We develop a relational pre-expectation calculus to upper bound the Kantorovich distance between two executions of a probabilistic program. We illustrate our methods by proving algorithmic stability of a machine learning algorithm, convergence of a reinforcement learning algorithm, and fast mixing for card shuffling algorithms. We also consider some extensions: proving lower bounds on the Total Variation distance and convergence to the uniform distribution. Finally, we describe an asynchronous extension of our calculus to reason about pairs of program executions with different control flow.
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
Aguirre, A., Haselwarter, P. G., Medeiros, M., Li, K. H., Gregersen, S. O., Tassarotti, J., Birkedal, L.
Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the probability of these errors, but existing verification approaches have limitations that lead to error probability bounds that are excessively coarse, or only apply to first-order programs. In this paper we present Eris, a higher-order separation logic for proving error probability bounds for probabilistic programs written in an expressive higher-order language. Our key novelty is the introduction of error credits, a separation logic resource that tracks an upper bound on the probability that a program returns an erroneous result. By representing error bounds as a resource, we recover the benefits of separation logic, including compositionality, modularity, and dependency between errors and program terms, allowing for more precise specifications. Moreover, we enable novel reasoning principles such as expectation-preserving error composition, amortized error reasoning, and error induction. We illustrate the advantages of our approach by proving amortized error bounds on a range of examples, including collision probabilities in hash functions, which allow us to write more modular specifications for data structures that use them as clients. We also use our logic to prove correctness and almost-sure termination of rejection sampling algorithms. All of our results have been mechanized in the Coq proof assistant using the Iris separation logic framework and the Coquelicot real analysis library.
Weakest Preconditions in Fibrations
Aguirre, A., Katsumata, S., Kura, S.
Weakest precondition transformers are useful tools in program verification. One of their key properties is composability, that is, the weakest precondition predicate transformer (wppt for short) associated to program f ; g should be equal to the composition of the wppts associated to f and g. In this paper, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy composability as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg–Moore monotone algebras. We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the nonempty powerset monad, the counter monad, or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.
