Tomás Vallejos Parada

I am a second-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. My general interests lie in formal verification, proof assistants, meta-programming, and having fun!

2026,

Jun 10

—

The week of 22th June I will be on a WG on formally verified computer algebra at FMPSI'26 in Paris

2026,

May 25

—

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)

2026,

Jan 17

—

I gave a talk at RocqPL'26 on an automatic generation of parametricity translations for inductive types (slides) (abstract)

2024,

Aug 30

—

I have a personal webpage!

2024,

Aug 05

—

My Master’s thesis appeared in the latest (issue) of the Bits Magazine, the outreach magazine of the Computer Science Department at the University of Chile (in Spanish). Check out the student’s section

News!