Étdues.txt

Études

================================================================================

1. Années

  • LDD1-LDD2 d'informatique mathématique (univ. Paris Saclay)
 2020-2022
  • LDD3 informatique mathématique (univ. Paris Saclay)
 2022-2023
  • LDD3 informatique mathématique (univ. Paris Saclay)
 2022-2023
  • M1 Master Parisien de Recherche en informatique (univ. Paris Saclay)
 2023-2024
================================================================================

2. Cours

Listes des cours important suivi trié par années, avec un petit résumé incomplet de chaque cours.

LDD3

--------------------------------------------------------------------------------
Éléments de logique pour l’informatique Cours de L3 donné par Christine Paulin-Mohring. Une introduction à l'automatisation des preuves avec le calculs des séquents 🔗.
Logique et informatique –
lambda-calcul		 Cours de la L3 de l'ENS donnée par Jean Goubault-Larrecq. Lambda-calcul non typé (confluence, ...) et typé (isomorphisme de Curry-Howard) 🔗.
Programmation Avancée Cours de programmation de l'ENS donnée par Jacques-Henri Jourdan et Armaël Guéneau. On voit des aspect avancé de OCaml (GADT, objet, type fantôme) et une introduction à Rust (appartenance, durée de vie, ...).
Informatique Théorique Cours de la LDD3 donnée par Laurent Rosaz. Cours sur les automates et les machines de Turing et les classes de complexité (NP-Complet, P-SPACE et NP-SPACE).
Compilation Cours de la LDD3 donnée par Thibaut BALABONSKI. On étudie la partie avant des compilateur (Lexer, Parser et Typage). On fini par faire un interpréteur d'un langage donnée (Miniml). 🔗.

M1

-------------------------------------------------------------------------------- ================================================================================

3. Stages

Formalisation des dictionnaires en Coq Stage au LMF Magistère 1 (2023)
Encadrant: Guillaume Melquiond
Sujet: Le stage visait à formaliser des dictionnaires en utilisant des tables de hachage grâce aux tableaux persistants de Coq.
Liens: sujet: 🖹 rapport: 🖹, presentation: 📽, git: ⌨
Micro Optimisation CompCert TER Stage au LMF Magistère 1 (2022-2023)
Encadrant: Guillaume Melquiond
Sujet: L'objectif du stage consistait à effectuer des micro-optimisations sur le compilateur prouvé en Coq, CompCert.
Liens: rapport: 🖹, git: ⌨