1 PhD topic

Under the supervision of Frédéric Blanqui and Gilles Dowek.

The broad topic is the translation of PVS specifications and proofs into the λΠ calculus modulo theory.

PVS is a an environment made of a theorem prover, a type checker and a parser which allows to develop specifications and prove them. It has been used by the NASA (see https://shemesh.larc.nasa.gov/fm/fm-pvs.html), Fujitsu &c. In particular, it implements predicate sub-typing, which allows to write concise specifications and provides a rich type system.

λΠ calculus modulo extends λ calculus with

• dependent types, which allows to have types that depend on terms (such as vectors of a given length);
• arbitrary reduction rules.

Pragmatically, the target of the translation is Dedukti, our implementation of the λΠ calculus modulo in OCaml.

An automatic translator is being developed. At the date of writing (August 2020), we translate 120kb of PVS’ standard library.

2 Teaching

At ENS Paris-Saclay in L3 and M1.

2.1 Se connecter aux machines 1S54

Pour que l’utilisateur user se connecte à la machine n de la salle 1S53,

ssh -AX n.dptinfo.ens-cachan.fr -J user@ssh.dptinfo.ens-paris-saclay.fr

Il est probable que vous ayez à rentrer 2 fois votre mot de passe. Pour s’éviter ça, mettez en place des clefs SSH.

2.2 Projet programmation 1

• TP0 (environnement de développement): PDF
• TP1 (OCaml, bases): PDF
• TP2 (fling): PDF, fichiers du projet
• TP4 (langage C): PDF
• TP5 (pointeurs): PDF, dynarray.h
• TP6 (assembleur): PDF HTML, avec un corrigé des programmes asm_corrections.tar.

Base de code du projet

2.2.1 Ressources pour Emacs

• Un fichier de configuration, à copier dans le dossier ~/.emacs.d/ (ne pas oublier de lancer opam user-setup install après avoir placé le fichier). Ce fichier utilise le gestionnaire de paquets straight.el qui permet une configuration déclarative (donc il suffit de mettre le fichier au bon endroit et de lancer emacs; ce sera emacs qui installera tous les paquets)
• Pour ceux qui veulent une distribution toute faite, allez voir Spacemacs (mode vim ou mode emacs), ou Doom emacs. Ces deux distributions fournissent un ensemble de paquets emacs pour obtenir un éditeur "fully featured" facilement (une petite configuration peut néanmoins rester nécessaire pour OCaml).

2.2.2 Cheatsheets

• shell
• vim
• emacs
• tuareg-mode
• ocaml
• ocaml stdlib

2.3 Architecture système

2.3.1 Pages de manuel

Le manuel Unix/Linux est une ressource inestimable pour ces TPs. Une question sur fork?

apropos fork
> fork (2)             - create a child process
> ...
man -s 2 fork

On peut aussi regarder les pages de manuel

• sur l’Internet, OpenBSD manpages
• sur gopher, OpenBSD manpages
• sur gemini Manpages

2.3.2 Les travaux pratiques

• TP 11-22 (Processus & signaux): PDF, Correction,
  Fichiers:
  • calc.zip,
  • touch\_weird.sh.x,
• TP 11-29 (Processus & tubes): PDF, Correction
  Fichiers:
  • shell.tar.gz
  • henon.p
    
• TP 12-5 (Fils et sémaphores): HTML, PDF, Correction,
  Fichiers:
  • mandel.tar.gz
  • henon.p
• TP 12-13 (Fils): HTML, PDF, Correction,
  Le script gnuplot pour tracer les ensembles de Julia (exécuter avec gnuplot julia.p et un fichier julia.dat contenant les données),
  Fichiers:
  • julia.p Pour tracer le contenu d’un fichier julia.dat, se trouvant dans le même fichier que julia.p: gnuplot julia.p,
  • ring.tar.gz,
• TP 12-19 (Réseau): PDF Correction,
  Fichiers:
  • ring.tar.gz,
  • packets.c
  • packets.h
• TP 01-10 (Révisions signaux): HTML PDF

2.3.3 Devoirs Maison

• Recoder un shell: voir exercice 5 du TP 11-29. À rendre le 2020-12-10 à 23:00 GMT+02, fichiers de départ.
• Compter les mots plus vite que Linux,
  Consignes et mwc.tgz.

2.4 Rewriting

• Lesson 1 (interpretation, termination): PDF, PDF (corrected), HTML, with implementation of mergesort in Dedukti3
• Lesson 2 (interpretation, termination): PDF, PDF (corrected) HTML
• Lesson 3 (multisets, recursive path ordering, well-founded induction): PDF, PDF (corrected), HTML
• Lesson 4 (dependency pairs): PDF, PDF (corrected), HTML
• Lesson 5 (critical pairs, completion): PDF, PDF (corrected), HTML
• Lesson 6 (orthogonality, decreasing diagrams): PDF, PDF (corrected), HTML

2.4.1 Homework

Homework, deadline: 2020-11-02, 12:00 GMT+01

2.5 Projet bases de données

Sujet

2.5.1 Dates

• 01/02/2021: Cahier des charges
• 01/03/2021: Analyse conceptuelle
• 12/05/2021: Rendu final

2.5.2 Supports de cours

• Analyse conceptuelle 1, avec son TD
• Analyse conceptuelle 2 sous typage, relation étendue, avec son TD
• Introduction à la programmation web

3 Publications

• Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-calculus Modulo Theory
• The new rewriting engine of Dedukti, with a link to the recording of FSCD presentation
• Efficient rewriting using decision trees implemented in Dedukti3.
• Airline disruption management with aircraft swapping and reinforcement learning, also available on HAL, with the slides and the code.
• Air traffic control partitioning with stochastic tree search

4 Contact

gabriel 🧶 hondet ✨ lsv 🧶 fr
Mastodon
GPG fingerprint: E5EA DC25 705C 8DDD CFD4 5700 31BC 8105 F659 D425