School Projects
Formalization of SystemF type safety using a logical relation in Coq (M2 project)
The actual implementation can be found in the Github repository. More details of the project are available on the written report. Knowledge about paper-proof of SystemF type safety using logical relations are expected. For an introduction to logical relations, I recommend to read the OPLSS 2023 lecture notes of the logical course taught by Amal Ahmed, and An Introduction to Logical Relations - Lau Skorstengaard.
DSL language MyCSV (M1 project)
MyCSV is a Domain Specific Language for CSV files manipulation. Its grammar is simple and intuitive, and provides basic operation over CSV files. This project is a part of the M1 course on DSL. The Github repository of the project (containing the report) is available here.
Compiler from subset of C to three-addresses like C code (L3 project)
Structit is a compiler from a front-end dialect of C language into 3-addresses like dialect of C. The front-end languages accepts basics type, pointers and structures. The back-end languages accepts int and void pointers types, and conditional/unconditional branches using if cond goto label and goto label. Full specification, sources and report are available in the Github repository here (in French).
Compiler from VSL+ to LLVM IR (M1 Project)
VSL+ (Very Simple Language Extended) is an Extended version of the language introduced by J.P Bennett in the book "Introduction to Compiling Techniques: a first course using ANSI C, LEX and YACC". Types allowed in VSL+ are integers and arrays or integers. The language provides functions (possibly recursive), conditionals, loops, blocks (with different scope level) and primitive READ and PRINT functions. The Gitlab repository of the project is not available.
NachOS (M1 Project)
Nachos OS is an instructional software distributed with a skeletal Operating System designed by the University of Berkeley. The aim of this project was to implement low level system features as: parallelism and synchronization, ACIA device driver, virtual memory (page default manager and replacement policy) and mapped filed.
On-the-fly modification (M1 Project)
Tool of code modification on-the-fly of a target process by another process, in C.
Compressor/Decompressor DNA sequence (M1 project)
Tool to compress and decompress DNA sequences in Python3. Sequences are stored as De Bruijn's graph. Two data structures can be used to index the graph: Bloom filter or FM-Index. A base sequence is used as reference, and similar sequences can be compressed, using the base sequence.