Valentin Blot
LS2N
Université de Nantes – faculté des Sciences et Techniques (FST)
Bâtiment 34
2 Chemin de la Houssinière
BP 92208, 44322 Nantes Cedex 3
office 34_211
contact(at)valentinblot(dot)org
Since September 2024, I am an INRIA permanent researcher (chargé de recherche) in the Gallinette team of the Laboratoire des Sciences du Numérique de Nantes (LS2N) at the Université de Nantes.
From March 2019 to August 2024, I was an INRIA permanent researcher (chargé de recherche) in the deducteam of the Laboratoire Méthodes Formelles (LMF) at the École Normale Supérieure Paris-Saclay.
From June 2018 to February 2019, I was a Marie Skłodowska-Curie fellow in the Institut de Recherche en Informatique Fondamentale (IRIF) at the Université Paris-Diderot, working with Hugo Herbelin on my research project "PolyBar: A new approach to polymorphism through bar recursion" (proposal, evaluation report).
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 799557
From Sep. 2017 to May 2018, I was a postdoctoral researcher in the Vals team of the Laboratoire de Recherche en Informatique (LRI) at the Université Paris-Sud, working with Chantal Keller and Stéphane Graham-Lengrand.
From Jan. 2017 to June 2017, I was a postdoctoral researcher in the Theory group of the School of Electronic Engineering and Computer Science at the Queen Mary University of London, working with Nikos Tzevelekos.
From Sept. 2014 to Dec. 2016 I was a postdoctoral researcher in the Mathematical foundations group of the computer science department at the University of Bath, working with Jim Laird.
From Sept. 2011 to Aug. 2014 I was a PhD student in the Plume team of the Laboratoire de l'Informatique du Parallélisme (LIP) at the École Normale Supérieure de Lyon under Colin Riba's supervising.
From Sept. 2007 to Aug. 2011 I was a student in the computer science department of the École Normale Supérieure de Lyon.
- Research
-
- Publications
-
- In peer-reviewed international conference proceedings
-
-
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory (HAL), with Gilles Dowek, Thomas Traversié and Théo Winterhalter, FoSSaCS 2024
-
Diller-Nahm bar recursion (HAL), FSCD 2023
-
Compositional pre-processing for automated reasoning in dependent type theory (HAL), with Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi and Pierre Vial, CPP 2023
-
A direct computational interpretation of second-order arithmetic via update recursion (HAL), LICS 2022
-
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types (HAL), with Jim Laird, LICS 2018
-
An interpretation of system F through bar recursion (HAL), LICS 2017 (implementation in coq and javascript)
-
Hybrid realizability for intuitionistic and classical choice (HAL), LICS 2016
-
Classical extraction in continuation models (HAL), FSCD 2016
-
On Bar Recursion and Choice in a Classical Setting (HAL), with Colin Riba, APLAS 2013
-
Realizability for Peano Arithmetic with Winning Conditions in HON Games (HAL), TLCA 2013
-
Quasi-Affine Transformation in Higher Dimension (HAL), with David Coeurjolly, DGCI 2009
- In peer-reviewed international journals
-
- In peer-reviewed international workshop proceedings
-
- In peer-reviewed national conference proceedings
-
- Scientific activities
-
- Steering committee
-
- Program committees
-
- Events organized
-
- Invited talk
-
- Supervisions
-
-
Thomas Laure, M2 internship, mar 2024 - aug 2024
-
Louise Dubois de Prisque, PhD student, sep 2020 - jul 2024, with Chantal Keller
-
Amélie Ledein, PhD student, feb 2021 - ongoing, with Catherine Dubois
-
Thomas Traversié, research curriculum at centrale-supelec, nov 2020 - sep 2023, with Gilles Dowek
-
Pierre Vial, post-doc, mar 2020 - sep 2022, with Chantal Keller
-
Amélie Rima, M2 internship, 2022
-
Boris Djalal, engineer, apr 2020 - apr 2022, with Chantal Keller
-
Simon Mirwasser, L3 internship, 2020, with Alexandre Miquel and Étienne Miquey
-
Étienne Miquey, post-doc, dec 2019 - oct 2020
-
Benjamin Graillot, M1 internship, 2019
-
Jui-Hsuan Wu, M1 internship, 2019, with Frédéric Blanqui
-
Quentin Garchery, M1 internship, 2018, with Chantal Keller
-
Amina Bousalem, M1 internship, 2018, with Chantal Keller
- Software development
-
- PhD thesis
-
- Game semantics and realizability for classical logic (HAL)
-
Committee:
- Internships
-
- 2011: ENS Lyon
-
My second master's internship was in the Plume team of the Laboratoire de l'Informatique du Parallélisme (LIP) at the École Normale Supérieure de Lyon under Colin Riba's supervising. I worked on the representation of functions on infinite sequences in the Hyland-Ong-Nickau game semantics. Here is my report.
- 2009: Radboud Universiteit Nijmegen
-
My first master's internship was in the Software Science group of the Institute for Computing and Information Sciences at the Radboud University Nijmegen under Freek Wiedijk's supervising. I worked on the formalization of algebraic numbers and Cayley-Hamilton and Liouville theorems in Coq. Here is my report, and here are the Coq sources .
- 2008: Université Lyon 1
-
My licence's internship was in the M2DisCo team of the Laboratoire d’InfoRmatique en Image et Systèmes d’information (LIRIS) at the Université Claude Bernard under David Coeurjolly's supervising. I worked on the quasi-affine transformations on pictures. Here is my report and here is the implementation of my work.
- Teaching
-
- 2017-2018
-
-
Practical work of Développement d'applications mobiles Android for 2nd year DUT students at IUT Orsay. Lecturer: Chantal Keller.
-
Practical work and tutorials of Introduction à l'algorithmique et à la programmation 1st year DUT students at IUT Orsay. Lecturers: Cécile Balkanski and Hélène Maynard.
- 2013-2014
-
- 2012-2013
-
- 2011-2012
-
- 2010
-
Success at the competitive exam of agregation de mathématiques with computer science option (rank 93).
- Scientific outreach (in french)
-
- Réalisation pratique
-
En mai 2013, j'ai travaillé pendant une semaine dans l'atelier Lyonnais de Pierre Gallais à la fabrication d'un atelier mathématique illustrant la non commutativité de certains groupes homotopiques, en passant par la résolution en pratique du problème suivant : comment accrocher un tableau à l'aide d'une corde et de deux clous, de telle manière que le retrait de n'importe lequel des deux clous fasse tomber le tableau. Voici une petite illustration de la solution, implémentée avec notre objet, et voici une extension dans le cas de trois clous. L'objet réalisé est maintenant utilisé dans le cadre de MathÀLyon : une équipe d'enseignants-chercheurs parcourant les collèges et lycées de la région lyonnaise afin de faire découvrir les mathématiques de manière ludique. J'ai moi-même participé à un atelier MathÀLyon au collège Marcel Aymé à Dagneux afin de présenter le nouvel objet.
- Stage Hippocampe
-
Du 5 au 7 juin 2013 j'ai participé à l'encadrement d'un stage hippocampe dans le laboratoire d'informatique de l'ENS Lyon. Nous accueillions une classe de seconde du lycée Robert Doisneau de Vaux-en-Velin afin de les faire réfléchir sur le concept d'infini. J'étais en charge d'un groupe de sept élèves qui ont travaillé sur les concepts d'infinis dénombrable et indénombrable, avant de présenter le fruit de leur réflexion sous forme de posters aux chercheurs et enseignants-chercheurs des laboratoires de mathématiques et d'informatique de l'ENS Lyon. Voici une photo de mon groupe, et une de leur poster.