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!

Our paper 'Functional correctness of an optimized modular inversion algorithm' j.w.w Assia Mahboubi, Guillaume Melquiond, and Pierre-Yves Strub was accepted at ITP26

Find the preprint here.

I gave a talk @RocqPL'26 on an automatic generation of parametricity translations for inductive types

Here are the slides and abstract.

I have a personal webpage!

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

You can find it in section “Estudiantes DCC”. Here is a link to the issue.

I wrote a how-to guide on connecting user-developed theories with MathComp ones, using the Hierarchy Builder.

You can find it on MathComp’s wiki, here is a link to the guide.

I earned my Master's degree in Computer Science and graduated as a Computing Engineer, both with the highest grade.

Here is a picture of that moment.

I have extended the autoinduct tactic, using MetaCoq, for the Rosetta stone of metaprogramming project @CUDW2023.

Autoinduct performs induction on the right argument of a recursive function. The tactic was originally used in a course by T. Ringer. Find a link to the implementation here.

News!