Valentin Blot

École Normale Supérieure Paris-Saclay
4, avenue des Sciences
91190 Gif-sur-Yvette
office 2S61
(+33)1 81 87 54 45
contact(at)valentinblot(dot)org

Since March 2019, I am 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).

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), 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

• A Semantics of 𝕂 into Dedukti (HAL), TYPES 2022 post-proceedings, 2023
• Realizability for Peano Arithmetic with Winning Conditions in HON Games (HAL), APAL, 2017
• Typed realizability for first-order classical analysis (HAL), LMCS, 2015

In peer-reviewed international workshop proceedings

• An Implementation of Set Theory with Pointed Graphs in Dedukti (HAL), with Gilles Dowek, and Thomas Traversié, LFMTP 2022
• General automation in Coq through modular transformations (HAL), with Louise Dubois de Prisque, Chantal Keller and Pierre Vial, PxTP 2021
• Quasi-Affine Transformation in 3-D: Theory and Algorithms (HAL), with David Coeurjolly and Marie-Andrée Jacob-Da Col, IWCIA 2009 (implementation)

In peer-reviewed national conference proceedings

• Vers une traduction de K en Dedukti (HAL), with Catherine Dubois and Amélie Ledein, JFLA 2022
• Bécassine à la chasse au Coq (démonstration d'un prototype) (HAL), with Louise Dubois de Prisque, Chantal Keller and Pierre Vial, JFLA 2022
• SMTCoq: automatisation expressive et extensible dans Coq (HAL), with Amina Bousalem, Quentin Garchery and Chantal Keller, JFLA 2019

Scientific activities

Steering committee

• LICS (Logic In Computer Science), workshop chair, 2023-

Program committees

• 31ièmes Journées Francophones des Langages Applicatifs (JFLA), 2020
• Syntax and Semantics of Low-Level Languages (LOLA), 2018
• 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS), 2018
• Games for Logic and Programming Languages XI (GaLoP), 2016

Events organized

• Journées du GT LHC (Groupe de Travail Logique, Homotopie, Catégories) du GdR IM (Groupement de Recherche Informatique Mathématique), local organizer, 2022
• Facets of realizability workshop, 2019, co-organized with Florian Steinberg

Invited talk

• Logic Colloquium, 2024, special session on proof theory

Supervisions

• Thomas Laure, M2 internship, mar 2024 - aug 2024
• 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
• Louise Dubois de Prisque, PhD student, sep 2020 - ongoing, with Chantal Keller
• 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

• My gitlab account (implementations of IWCIA'09 and LICS'17)
• A proof of Liouville's theorem in Coq
• SMTCoq
• A type-checker and interpreter of the simply-typed lambda-calculus
• Normalization of System F, formalized in coq

PhD thesis

Game semantics and realizability for classical logic (HAL)

Committee:

• Pierre-Louis Curien (president)
• Pierre Hyvernat
• Olivier Laurent (director)
• Andrzej Murawski (reviewer)
• Colin Riba (supervisor)
• Thomas Streicher (reviewer)

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

• Practical work of Algorithmique et Programmation Impérative, Initiation for 1st year licence students at the Université Claude Bernard. Lecturer: Elodie Desserée.
• Lectures of Projet2 (programming a SAT solver) for 3rd year licence students at the École Normale Supérieure de Lyon. Co-lecturer: Daniel Hirschkoff.

2012-2013

• Tutorials of Architecture, Système, Réseau (ASR) for 3rd year licence students at the École Normale Supérieure de Lyon. Lecturer: Nicolas Estibals.
• Tutorials of Logic for 3rd year licence students at the École Normale Supérieure de Lyon. Lecturer: Alexandre Miquel.

2011-2012

• Practical work of Algorithmique et Programmation Impérative, Initiation for 1st year licence students at the Université Claude Bernard. Lecturer: Elodie Desserée.
• Tutorials of Logique classique for 3rd year licence students at the Université Claude Bernard. Lecturer: Emmanuel Coquery.
• Tutorials of Logic for 3rd year licence students at the École Normale Supérieure de Lyon. Lecturer: Alexandre Miquel.

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.