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 Course given by Christine Paulin-Mohring.
An introduction to the automation of proofs with sequential calculus. 🔗
Logic and computing -
lambda-calculus		 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 Course given by Laurent Rosaz.
Course on automata and Turing machines Turing machines and complexity classes (NP-Complete, P-SPACE and NP-SPACE).
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.
Lambda-calculus and categories Course at the ENS given by Paul-André Melliès.
Basic aspects of categories theories for formalizing the lambda-calculus with this theory. 🔗
Lambda-calculus 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 (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: ⌨