About me


I am Basile Pesin, a computer science PhD student in ENS Ulm. I am interested in programming languages, compilers and proof assistants. In particular, I am currently working on formalizing the semantics of SCADE-style state machines in the Coq proof assistant, as part of the Velus project. I also enjoy working on various subjects, such as functional or logic programming, or programming embedded devices. Because programming isn't everything, I also take some time for rock-climbing, baking or reading.


Since 2020, I've been teaching a few undergrad courses at Sorbonne Université (in french):



  • [VPVC:VMIL:2020] Steven Varoumas, Basile Pesin, Benoit Vaugon & Emmanuel Chailloux, Programming Microcontrollers through High-Level Abstractions, , (2020).
  • [BCPT:FC:2020] Bruno Bernardo, Raphaël Cauderlier, Basile Pesin & Julien Tesson, Albert, An Intermediate Smart-Contract Language for the Tezos Blockchain, , 12063, 584-598 (2020). link.
  • [BRHPT:FM:2019] Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin & Julien Tesson, Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts, , 12232, 368-379 (2019). link.
  • [BJPP:JFLA:2021] Timothy Bourke, Paul Jeanmaire, Basile Pesin & Marc Pouzet, Normalisation vérifiée du langage Lustre, , (2021). link.


You can reach me by email at basile.pesin@vertmo.org

Auteur: Basile Pesin

Created: 2021-04-12 lun. 11:15