News | Tomás Vallejos Parada

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

Here are the slides and abstract.

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)](https://hal.science/hal-05554365/)

Find the preprint here.

I gave a talk at RocqPL'26 on an automatic generation of parametricity translations for inductive types [(slides)](/slides/26/slides-26rocqpl-trocq-param.pdf) [(abstract)](/papers/26/abstract-26rocqpl-trocq-param.pdf)

Here are the slides and abstract.

I have a personal webpage!

My Master's thesis appeared in the latest [(issue)](https://www.dcc.uchile.cl/difusion/revista/26) 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

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

I wrote a [(how-to)](https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances) 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!