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


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.


Some stuff hacked in OCaml

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