É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: ⌨
|