Tomás Vallejos

I am a first-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 algorithms dealing with mathematical objects applying low-level optimizations.

My general interests lie in formal verification, proof assistants, meta-programming, and having fun!

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!