Thomas Rubiano

I did a double PhD program in the LIPN at Université Paris 13 and DIKU at university of Copenhagen. I’ve worked on Implicit Computational Complexity theories and compilers. This thesis was supervised by Jean-Yves Moyen, Virgil Mogbile and Jakob Grue Smonsen, it was funded by the ELICA ANR project.

I’ve worked at the IRISA in the Celtique Team as PostDoc funded by the DISCOVER ANR project . I’ve worked with Delphine Demange on analysis and certification techniques with coq using different compilers. We’ve implemented and formalized an intermediate representation called SSAFire and built from CompcertSSA. This form of program is also called synchronous value graph, it eases the transformation expressions then their formalizations.

I’ve also worked on the WebAssembly semantic with Alan Schmitt and Thomas Jensen. Described in skel, a language describing the skeletal semantic of a language, and using the necro project, we were able to generate interpreters and coq formalizations around it.

Then I was Research Ingineer at CNRS working on Squirrel-Prover and its Js version with David Baelde and Stéphanie Delaune.

I'm currently SRP at Inria working on Code Generation and Annotation in Compilers for Security concerns. This work takes part of the Lot 3 of the PEPR Arsene. It is supervised by Erven Rohou, Damien Hardy and Ronan Lashermers.

Contact

Curriculum Vitae

You can find my CV here.