Lionel Rieg
Presentation
Since September 2018, I am a Maître de Conférence (associate professor) in the Verimag laboratory and at Grenoble-INP – Ensimag.
Previously, I have been:
- associate research scientist at Yale University in the FLINT group, from September 2016 to August 2018;
- post-doc at the Collège de France with Gérard Berry, from September 2014 to August 2016;
- ATER (teaching and research assistant) at the ENSIIE and the CÉDRIC (CPR team,Conception et Programmation Raisonnées), from September 2013 to August 2014;
- PhD student at the ENS de Lyon under the supervision of Alexandre Miquel (who left for Uruguay since that time), from September 2010 to August 2013.
Research Interests
NEW: Internship opportunities for 2025!
Design and Evaluation of Strategies for Automated Proofs using Reasoning Modulo EquivalenceExploration by model-checking of timing anomaly cancellation in a processor- Analyzing fault parameters triggering timing anomalies
- Sûreté des essaims de robots mobiles
The most up-to-date list of my publications can be found on DBLP.
Formal Proofs about Robot Swarms
The Pactole project aims at formalizing results about robot swarms in a unified framework. This framework supports both impossibility proofs (for instance, impossibility of gathering on a real line) and proofs of algorithms (for instance, gathering in the plane).
Formal Proofs about the Compilation of Synchronous Languages
- Formalizing the compilation of Esterel towards digital circuits, the final objective being to extract a proven compiler, in the style of CompCert.
- Formalization of the compilation of Lustre towards imperative code, in particular towards CompCert intermediate language Clight.
Congruence for setoid equalities
This project aims at extending the congruence tatic for Coq to arbitrary types equipped with a setoid structure.
This raises several questions:
- how to handle existing algorithms to multiple relations?
- how to handle multiple equivalence relations on the same type and their interplays?
- …
A prototype of this work was presented at the Coq workshop 2020.
PhD Work
The research theme of my PhD is Krivine's classical realizability, more precisely the computational content of forcing inside this framework. I have also worked on introducing real numbers inside the KAM (Krivine Abstract Machine).
I have formalized <a href="Herbrand-proof/v.8.3/">a (classical) proof of Herbrand's theorem</a> inside the Coq proof assistant which, after extraction, gives a certified algorithm in the λc-calculus computing herbrand trees. The directory also contains a makefile and a file to optimize realizers during extraction by kextraction.
Since then, I got a proof by forcing which does not use the fan theorem and from which one can extract a realizer thanks to the forcing translation.
Manuscript
My manuscript is entitled On Forcing and Classical Realizability.
It is available here for a color-version and there for a printer-friendly version.
Additional documents are as follows:
- the classical realizability library in Coq
- a quick formalization of forcing combinators:
- here for a forcing structure,
- there for a forcing datatype,
- the common file for both formalizations.
PhD defense
My defense took place on June, 17th, 2014 at 14h30 in the D amphitheatrum of the ENS de Lyon.
As I was asked for them, here are the slides of my defense.
Teaching (in French)
L'accès à certaines pages peut nécessiter un compte à Grenoble-INP-UGA.
- Théorie des Langages 1
- Introduction à la sécurité
- Architecture : circuits numériques et éléments d'architecture
- Conception et Exploitation des Processeurs
- Cours d'informatique au semestre 4 de la Prépa INP
- Magistère d'informatique
Années passées
Les liens sont probablement cassés depuis le temps, sauf les liens locaux (et encore…).
ENSIIE (2014-2016)
Bien que n'étant plus à l'ENSIIE, j'y redonne quelque cours et TD.
- Langages Formels Je donne les TD de Langages Formels à l'antenne ENSIIE de Strasbourg, dont le cours est assuré par Xavier Urbain.
- Logique Je m'occupe d'un groupe de TD de Logique à l'ENSIIE, dont le cours est assuré par Julien Forest.
- Modèles de Calcul Enfin, je m'occupe avec Xavier Urbain des cours et TD de Modèles de Calcul.
ENSIIE (2013-2014)
ATER à l'ENSIIE, j'y ai donné des TD/TP et quelques cours en première et deuxième année.
- TD d'Optimisation Mathématique, cours assuré par Alain Faye
- TD 2: Convexité (sujet, corrigé)
- TD 3: Problème géomètrique dual et méthode des moindres carrés (sujet, corrigé)
- TD 4: Méthodes itératives (sujet, corrigé)
- TD 5: Méthodes itératives quasi-Newtoniennes (sujet)
- TD 6: Qualification de Arrow-Hurwicz-Uzawa (sujet, corrigé)
- TD 7: Conditions d'optimalité et relaxation (sujet, corrigé)
- TD 8: Méthodes duales et primales (sujet, corrigé)
- TD 10: Gradient réduit et méthode de pénalité (sujet, corrigé)
- TD 11: Méhodes de pénalité et de barrière (sujet, corrigé)
- Autres cours de première année
- TD/TP de IPI (Informatique: Programmation Impérative), cours assuré par Xavier Urbain;
- TD/TP de IPF (Informatique: Programmation Fonctionnelle), cours assuré par Xavier Urbain;
- TP de IPA (Informatique: Programmation Avancée), cours assuré par Guillaume Burel
- Projet Mathématique (sur une journée), responsable: Thomas Lim;
- Projet Informatique (éditeur collaboratif), responsable: Guillaume Burel.
- Cours de deuxième année
- TD/TP de Compilation, cours assuré par Guillaume Burel;
- TD/TP de Validation et Vérification du Logiciel, cours assuré par Guillaume Burel;
- TD de Langages Formels, cours assuré par Xavier Urbain;
- Cours/TD de Modèles de Calcul, cours assuré par Pierre Courtieu, Xavier urbain et moi-même.
ENS de Lyon (2012-2013)
- Preuves sur ordinateur
Je donne au premier semestre les TD/TP pour le cours de Preuves sur ordinateur donné par Colin Riba.
- λ-calcul et codage des types de données (sujet.pdf et corrigé.pdf)
- Réduction du sujet, correspondance de Curry-Howard et théorème de Glivenko (sujet.pdf)
- Reprise de Curry-Howard et induction dans HA (sujet.v ou sujet.html et corrigé.v)
- Tactiques automatiques et division entière (sujet.v ou sujet.html et corrigé.v))
- Filtrage dépendant (sujet.v ou sujet.html et corrigé.v)
- Le prédicat d'accessiblité Acc (sujet.v ou sujet.html et corrigé.v)
- Codages de types de données dans système F (sujet.pdf et corrigé.pdf)
- IPP et preuves par réflection (sujet.v ou sujet.html)
- Calcul des séquents (sujet.pdf et corrigé.pdf)
- Réversibilités dans LK₀ (sujet.pdf et corrigé.pdf)
- Théorème de Herbrand (sujet.pdf et corrigé.pdf)
- Résolution (sujet.pdf et corrigé.pdf)
- Introduction à l'Informatique
Je donne également au premier semestre les TP pour le cours d'Introduction à l'Informatique donné par Stephan Thomasse dans le cadre du master Systèmes Complexes.
- Introduction à l'informatique théorique
Toujours au premier semestre, je donne les cours/TD/TP pour le cours Introduction à l'informatique théorique de la classe passerelle avec Guillaume Hanrot.
- Initiation réseaux et base de données
Enfin, je donne des TP dans le cours d'Initiation réseaux et base de données donné par Fabien Duchateau à l'UCBL.
ENS de Lyon (2011-2012)
- Évaluation de performances
Je donne à nouveau au premier semestre des TD pour le cours d'Évaluation de Performance donné par Éric Thierry.
- Rappels de probabilités (notions usuelles, paradoxes, lois classiques) (sujet et corrigé)
- Suite du premier TD
- Simulation de variables aléatoires et modélisation par schéma de Matthes (sujet et corrigé)
- Schéma de Matthes et chaînes de Markov discrètes à nombre d'états fini (sujet et corrigé)
- Étude générale du comportement asymptotique des chaînes de Markov discrètes à nombre d'état fini (sujet et corrigé)
- Théorèmes de Foster et protocole ALOHA discret (sujet et corrigé)
- Correction du partiel du 9 novembre
- Processus de Poisson et file M/M/1 (sujet et corrigé)
- Analyse et comparaison de files d'attente (sujet et corrigé)
- Files M/M/c et réseaux de Jackson (sujet et corrigé)
- Rattrapage d'un cours à la place du TD
- Réseaux de Pétri (sujet et corrigé)
ENS de Lyon (2010-2011)
- Évaluation de performance
Je donne au premier semestre des TD pour le cours d'Évaluation de Performance donné par Éric Thierry.
- Rappels de probabilités (sujet et corrigé)
- Lois classiques (sujet et corrigé)
- Cours sur la simulation de variables aléatoires à partir d'une loi uniforme
- méthode de l'inverse
- méthode du rejet
- méthode de l'alias (simulation en temps constant d'une loi à support fini)
- Schémas de Matthes et chaînes de Markov (sujet et corrigé)
- Modélisation et chaînes de Markov discrètes (sujet et corrigé)
- Correction du partiel du 4 novembre
- Théorèmes de Foster et protocole ALOHA discret (sujet et corrigé)
- Chaînes de Markov en temps continu (sujet et corrigé)
- Loi de Little et réseaux de Petri (sujet et corrigé)
- Programmation 2
Au second semestre, je m'occupe, avec Paolo Tranquilli, des TD du cours de Programation 2 donné parPierre Lescanne.
- Systèmes de Hilbert
- Déduction naturelle
- Modèle de Kripke et traduction de Gödel
- Machines de Turing et compilation
- Machines RAM et théorème de Rice
- Minimisation et fonction d'Ackermann
- Fonction d'Ackermann, problème du mot et λ-définissabilité
- Pavages et degrés Turing
- Révisions en vue du partiel
- Réécriture abstraite
- Terminaison et unification
- Unification et terminaison
- Bases de Gröbner et complétion
- Correction du partiel du 12 avril
- Sémantique axiomatique et logique de Hoare
Lycée du Parc (2008-2009)
Je donne les TPs de Caml Light> au Lycée du Parc dans le cours d'informatique de MP/MP* assuré par Stéphane Gonnord.
- Prolégomènes et Piles (sujet et corrigé)
- Logique et circuits (sujet et corrigé)
- Cryptographie par RSA (sujet et corrigé)
- suite du TD précédent
- Compression de niveaux de gris (sujet et corrigé)
- Multiplication de polynômes (sujet et corrigé)
- Fractales (sujet et corrigé)
- Recherche de motif dans un texte (sujet et corrigé)
How to Contact Me
- By e-mail: firstname.lastname@univ-grenoble-alpes.fr
- By phone: 04 57 42 22 09