News | Tomás Vallejos Parada

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!