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.
Contact/Personal information
Email: armael dot gueneau at ens-lyon dot fr
Internships
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](Hybrid Separation Logic report.pdf), and [the slides](Hybrid Separation Logic slides.pdf).
M2: Formal Verification of Asymptotic Complexity Bounds for OCaml Programs, supervised by François Pottier and Arthur Charguéraud. [The report](Formal Verification of Asymptotic Complexity Bounds for OCaml Programs report.pdf) and [the slides](Formal Verification of Asymptotic Complexity Bounds for OCaml Programs slides.pdf).
Programming
Some stuff hacked in OCaml
- Stone, a very simple and stupid static webpages generator. This page was created using it.
- Papiers, a tool I use to index all my pdfs (that I put in the same directory), and quickly search through them.
ENS L3 project
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.
ENS M1 project
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).
Some friends
