Tomás Vallejos Parada

I am a third-year PhD student on the Gallinette team working towards reconciling efficiency and trust for algorithms in Computer Algebra Systems, under the supervision of Assia Mahboubi. Currently, I am exploring the limits of formal verification tools for verifying low-level optimized algorithms whose correctness is justified with high-level mathematical objects.

I co-organize FormAL, monthly seminars on formal methods and programming languages in latin america. My general interests lie in formal verification, proof assistants, meta-programming, and having fun!


Last updated: 16 Sep 2026
—
I presented our paper ‘Functional correctness of an optimized modular inversion algorithm’ at ITP'26, part of FLoC'26 (paper) (slides)
—
I was at the Summer School on Foundations of Programming and Software Systems at FLoC'26
—
The week of 22th June I will be on a WG on formally verified computer algebra at FMPSI'26 in Paris
—
Our paper ‘Functional correctness of an optimized modular inversion algorithm’ j.w.w Assia Mahboubi, Guillaume Melquiond, and Pierre-Yves Strub was accepted at ITP'26 (preprint)
—
I visited Enrico Tassi and gave a talk on the functional correctness of an optimized modular inversion algorithm (slides)