Studies.txt
Studies
================================================================================
1. Years
- (Y1-2) Double degree in computer science and
mathematics (univ. Paris Saclay)
|
2020-2022 |
- (Y3) Double degree in computer science and
mathematics (univ. Paris Saclay)
|
2022-2023 |
- Mag 1 computer science (univ. Paris Saclay)
|
2022-2023 |
- M1 Parisian Master of Research in Computer Science
(univ. Paris Saclay)
|
2023-2024 |
================================================================================
2. Courses
Lists of important courses followed, sorted by year, with a short
summary for each course.
LDD3
--------------------------------------------------------------------------------
| Elements of logic for computing |
L3 course given by Christine
Paulin-Mohring. An introduction to the automation of proofs
with sequential calculus
🔗.
|
Logic and computing -
lambda-calculus |
L3 course at the ENS given by Jean
Goubault-Larrecq. Untyped (confluence, ...) and typed lambda-calculus
(Curry-Howard isomorphism)
🔗.
|
| Advanced programming |
ENS programming course given by Jacques-Henri Jourdan and Armaël
Guéneau. Advanced aspects of OCaml (GADT, Object, ghost type) and an
introduction to Rust (ownership, lifetime, ...).
|
| Theoretical computing |
LDD3 course given by Laurent Rosaz. Course on automata and Turing
machines Turing machines and complexity classes (NP-Complete, P-SPACE
and NP-SPACE).
|
| Compilation |
LDD3 course given by Thibaut BALABONSKI. We study the front end of
compilers (Lexer, Parser and Typing). We finish by making an
interpreter of a given language (Miniml).
🔗.
|
M1
--------------------------------------------------------------------------------
================================================================================
3. Intership
| Formalizing dictionaries in Coq |
Intership at LMF Mag 1 (2023)
Supervisor: Guillaume Melquiond
Subject:
The aim of the course was to formalise dictionaries using
hash tables using Coq's persistent tables.
Link:
subject: 🖹
report: 🖹,
presentation: 📽,
git: ⌨
|
| CompCert Micro Optimisation |
TER at LMF Mag 1 (2022-2023)
Supervisor: Guillaume Melquiond
Subject:
The aim of the internship was to carry out micro-optimisations
on the proven Coq compiler, CompCert.
Link:
report: 🖹,
git: ⌨
|