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  Course given by Christine
PaulinMohring. An introduction to the automation of proofs with sequential calculus. 🔗 
Logic and computing  lambdacalculus 
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  Course given by Laurent Rosaz. Course on automata and Turing machines Turing machines and complexity classes (NPComplete, PSPACE and NPSPACE). 
Compilation  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
Programming languages, semantics and compilers  Course given by Thibaut Balabonski. We study the backend of compilers with assembly code generation (register allocation, ...), We finish by making an optimizing compiler. 🔗 
Reactive programming  Course at the ENS given by Marc Pouzet and Timothy Bourke. The aim of this course is to study and implement the fundamental principles and models used to design and build reactive systems. 
Lambdacalculus and categories  Course at the ENS given by PaulAndré Melliès. Basic aspects of categories theories for formalizing the lambdacalculus with this theory. 🔗 
Lambdacalculus  Course given by Thibaut Balabonski. Lambda calculus semantics and computation power. 🔗 
Automates and applications  Course given by Kim Hguyễn. Introduction to automata, their properties as algebraic as algebraic objects and their applications as computational objects. 🔗 
3. Intership
Verified interoperability with exceptions between OCaml and C 
Intership at LMF M1 (2024) Supervisor: Armaël Guéneau Subject: The aim of the internship was to extend Melocoton with exceptions, and to test this extension with simple examples Link: subject: 🖹 report: 🖹, presentation: 📽  📽, git: ⌨ 
Formalizing dictionaries in Coq 
Intership at LMF Mag 1 (2023) Supervisor: Guillaume Melquiond Subject: The aim of the internship 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: ⌨ 