Studies.txt
Studies
================================================================================1. Years

20202022 

20222023 

20222023 

20232024 
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 PaulinMohring. An introduction to the automation of proofs with sequential calculus 🔗. 
Logic and computing  lambdacalculus 
L3 course at the ENS given by Jean GoubaultLarrecq. Untyped (confluence, ...) and typed lambdacalculus (CurryHoward isomorphism) 🔗. 
Advanced programming  ENS programming course given by JacquesHenri 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 (NPComplete, PSPACE and NPSPACE). 
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 (20222023) Supervisor: Guillaume Melquiond Subject: The aim of the internship was to carry out microoptimisations on the proven Coq compiler, CompCert. Link: report: 🖹, git: ⌨ 