/* @licstart The following is the entire license notice for the JavaScript code in this tag. Copyright (C) 2012-2020 Free Software Foundation, Inc. The JavaScript code in this tag is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License (GNU GPL) as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. The code is distributed WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU GPL for more details. As additional permission under GNU GPL version 3 section 7, you may distribute non-source (e.g., minimized or compacted) forms of that code without the copy of the GNU GPL normally required by section 4, provided you include this license notice and a URL through which recipients can access the Corresponding Source. @licend The above is the entire license notice for the JavaScript code in this tag. */

Lionel Rieg

Table des matières

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:

Research Interests

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:

  1. the classical realizability library in Coq
  2. 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.

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
    1. TD 2: Convexité (sujet, corrigé)
    2. TD 3: Problème géomètrique dual et méthode des moindres carrés (sujet, corrigé)
    3. TD 4: Méthodes itératives (sujet, corrigé)
    4. TD 5: Méthodes itératives quasi-Newtoniennes (sujet)
    5. TD 6: Qualification de Arrow-Hurwicz-Uzawa (sujet, corrigé)
    6. TD 7: Conditions d'optimalité et relaxation (sujet, corrigé)
    7. TD 8: Méthodes duales et primales (sujet, corrigé)
    8. TD 10: Gradient réduit et méthode de pénalité (sujet, corrigé)
    9. 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)

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.

    1. Rappels de probabilités (notions usuelles, paradoxes, lois classiques) (sujet et corrigé)
    2. Suite du premier TD
    3. Simulation de variables aléatoires et modélisation par schéma de Matthes (sujet et corrigé)
    4. Schéma de Matthes et chaînes de Markov discrètes à nombre d'états fini (sujet et corrigé)
    5. Étude générale du comportement asymptotique des chaînes de Markov discrètes à nombre d'état fini (sujet et corrigé)
    6. Théorèmes de Foster et protocole ALOHA discret (sujet et corrigé)
    7. Correction du partiel du 9 novembre
    8. Processus de Poisson et file M/M/1 (sujet et corrigé)
    9. Analyse et comparaison de files d'attente (sujet et corrigé)
    10. Files M/M/c et réseaux de Jackson (sujet et corrigé)
    11. Rattrapage d'un cours à la place du TD
    12. Réseaux de Pétri (sujet et corrigé)

ENS de Lyon (2010-2011)

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.

  1. Prolégomènes et Piles (sujet et corrigé)
  2. Logique et circuits (sujet et corrigé)
  3. Cryptographie par RSA (sujet et corrigé)
  4. suite du TD précédent
  5. Compression de niveaux de gris (sujet et corrigé)
  6. Multiplication de polynômes (sujet et corrigé)
  7. Fractales (sujet et corrigé)
  8. 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