I studied computer science from 2012 to 2016 at the École Normale Supérieure de Lyon. My interests include programming languages, proofs of programs, compilation and operating systems.
Email: armael dot gueneau at ens-lyon dot fr
L3: Internship at Gallium, under the supervision of François Pottier and Jonathan Protzenko. I worked on iterators in Mezzo, which led to a presentation at the HOPE workshop (talk proposal, slides). The internship report can be found here.
M1: Hybrid Separation Logic, with Jules Villard at ICL. The report, and the slides.
M2: Formal Verification of Asymptotic Complexity Bounds for OCaml Programs, supervised by François Pottier and Arthur Charguéraud. The report and the slides.
During the ENS L3 programmation project, we played a bit with the DPLL algorithm. The result is this slow, heavy, not optimized SAT-solver we (I and Antoine Pouille) programmed, which also incorporates things (as plugins, every functionnality including heuristics is a dynamically-loaded plugin) like graph coloration or SMT linear constraints solving.
The ENS M1 project is more ambitious, and involves forming groups of around 8 to 15 people, then trying to achieve a somewhat ambitious and innovative programming project. Thus illustrating the joy and virtues (or not) of managing a group and defining workpackages. In our case it didn't end too bad; we developed a prototype for an origami simulator and diagram creator, Origram.
These days I'm in the process of rewriting the non-GUI part of the program in OCaml, instead of C++ (in the ml branch).