Étdues.txt
Études
================================================================================1. Années
|
2020-2022 |
|
2022-2023 |
|
2022-2023 |
|
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 donné par Christine Paulin-Mohring. Une introduction à l'automatisation des preuves avec le calculs des séquents 🔗. |
| Logique et informatique – lambda-calcul |
Cours 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 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 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
--------------------------------------------------------------------------------| Langages de programmation, sémantique et compilateur | Course donné par Thibaut Balabonski. On étudie la partie arrière des compilateurs avec la génération de code assembleur (allocation de registre). On finit le cours en faisant un compilateur optimisant d'un langage impératif. 🔗 |
| Programmation réactive | Cours à l'ENS donné par Marc Pouzet and Timothy Bourke. L’objectif de ce cours est l’étude et la mise en œuvre des principes et modèles fondamentaux utilisés pour concevoir et réaliser les systèmes réactifs. |
| Lambda-calcul et catégories | Cours à l'ENS ENS donné par Paul-André Melliès. Aspects basique de théorie des catégories pour formaliser le lambda-calcul dans cette théorie. 🔗 |
| Lambda-calcul | Cours donné par Thibaut Balabonski. Sémantique du lambda-calcul et son pouvoir expressif. 🔗 |
| Automates et applications | Cours donné par Kim Hguyễn. Ce cours présente une introduction aux automates, leurs propriétés en tant qu'objets algébriques et leurs applications en tant qu'objets calculatoires. 🔗 |
3. Stages
| Interopérabilité vérifiée avec les exceptions entre OCaml et C | Stage au LMF M1 (2024) Encadrant: Armaël Guéneau Sujet: Le stage visait à étendre Mélocoton avec des exceptions et tester cette extension avec des exemples simple. Liens: sujet: 🖹 rapport: 🖹, présentation: 📽 - 📽, git: ⌨ |
| 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: 🖹, présentation: 📽, 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: ⌨ |