Projects

Work projects

Verified code generation for the polyhedral model (2018).

Implementation and verification in Coq of the code generation step in the polyhedral model. This work was done during my 2018 internship in the Gallium research team under the supervision of Xavier Leroy. Here are the report, the slides for the internship defense (both in French), and the paper (DOI, mirror) we published at POPL21 about it.

Verified code generation for the PVS2C code generator (2017).

Implementation and verification in PVS of an idealized version of the PVS2C code generator. This work was done during my 2017 internship in the CSL team, under the supervision of Natarajan Shankar. Here are the report, the slides for the internship defense and the paper (DOI, mirror) we published about it after some additional work by Antoine Séré.

Improved widening operators for proving termination by abstract interpretation (2016).

Design and implementation of improved widening operators for the FuncTion tool, an analyser for C programs based on abstract interpretation for deriving sufficient preconditions for termination, guarantee and recurrence properties. This work was done during my 2016 internship in the Chair of Programming Methodology at ETH Zürich, under the supervision of Caterina Urban. Here are the report and slides for the intership defense, as well as slides for an audience unfamiliar with abstract interpretation, and the paper we published at TACAS 2017 to present the results (DOI, mirror).

School projects

Compiler for a small functional language (2018).

Implementation of a compiler for a small functional language for the Functional programming and type systems course of the MPRI, given by François Pottier, Didier Rémy, Yann Régis-Gianas and Pierre-Évariste Dagand. The language being compiled supports curried functions, algebraic datatypes with deep pattern matching, algebraic effects (archive) with multishot continuations, and a static type system based on MLsub (DOI) with type and effect inference, including subtyping. It also includes a generational garbage collector, but only the minor collection is implemented, and memory in the major heap is never reclaimed. The report (in French) contains some additional information, including the typing rules.

Topological sort in Why3 (2018).

Implementation and verification of topological sorting using Why3. This was done as a project for the Proof of programs (part 1, part 2) course of the MPRI, given by François Bobot and Jean-Marie Madiot. The report (in French) contains some explainations on the invariants used to prove correctness.

Verification of results on Peano and Heyting arithmeting in Coq (2017).

Specification of Peano and Heyting arithmetic, proof of some basic facts, as well as that Peano arithmetic is Π₀²-conservative over Heyting arithmetic, verified using Coq. This was done as a project for the Foundation of proof systems course of the MPRI, given by Benjamin Werner and Pierre-Yves Strub.

Verification of a weakest-precondition generator for the While language in Coq (2017).

Executable weakest-precondition generator for the While language, written and verified using Coq. This was done as a project for the Foundation of proof systems course of the MPRI, given by Benjamin Werner and Pierre-Yves Strub.

Distributed multiple voting (2017), with Noémie Fong

Implementation and simulations of distributed multiple voting, based on this paper (DOI). This project was for the Modèles et algorithmes des réseaux course at ENS, given by Ana Bušić, Marc Lelarge and Rémi Varloot. Here is the report (in French) for this project.

Algorithms for the travelling salesman problem (2017), with David Saulpic

Implementation of an exact, dynamic programming solution for the travelling salesman problem, as well as two heuristics, and a method to find lower bounds using the dual linear program. This project was for the Optimisation convexe et combinatoire (part 1, part 2) course at ENS, given by Alexandre d'Aspremont and Zhentao Li. Here are the project statement (archive), which can contain useful information on the algorithm used to find lower bounds, the report, and the slides for this project (all in French).

Minimalistic bootable kernel for the Raspberry Pi (2016), with Théophile Bastian.

Implementation of a minimalistic kernel for the Raspberry Pi, for the Systèmes et réseaux course at ENS, given by Marc Pouzet and Timothy Bourke. The kernel handles processes (with round-robin scheduling), a network stack handling ping and UDP, an in-memory filesystem that can contain executable files, a minimalistic shell, as well as a server for multiplayer snake server, and a basic implementation of the Z-machine, which allows playing a number of text adventure games. More information can be found in the report (in French).

Small SMT solver for equality logic (2016).

Implementation of a small SMT solver for equality logic (subset of the theory of uninterpreted functions when there are no function symbols and all that remains is the reflexivity, symmetry and transitivity of the equality). The project was written for the Sémantique et applications à la vérification course at ENS, given by Xavier Rival, Antoine Miné and Sylvain Conchon. Some technical information on the implementation can be found in the project report (in French).

Optimising compiler from a small subset of Scala to x86-64 assembly (2015), with Noémie Cartier.

Implementation of an optimising compiler from a small subset of Scala to x86-64 assembly. This project was written for the Langages de programmation et compilation course at ENS, given by Jean-Christophe Filliâtre and Robin Morisset. The compiler features static typing, register allocation, and a few common optimisations such as constant propagation. Additional information on the subset of Scala being compiled can be found in the project statement (part 1 (archive), part 2 (archive)), and technical information on the implementation choices can be found in the three parts of the report (parsing and typing, code generation, optimisation) (all in French).

Clock program in assembly, running on a custom processor, running on a circuit simulator (2015), with Théophile Bastian and Noémie Cartier.

Implementation of a logic circuit simulator, written as a netlist-to-C compiler, design and specification of a processor in this netlist language, inspired by the ARM architecture, implementation of an assembler for this processor and a clock program hand-written in assembly to demonstrate it. This project was written for the Système digital : de l'algorithme au circuit course at ENS, given by Jean Vuillemin and Timothy Bourke. Technical information about the project can be found in the three parts of the report (simulator, processor architecture, final report), less technical information can be found on the slides (all in French).

Partial evaluator for a small lisp-like language (2015).

Implementation of a small Lisp-like language, with an interpreter, a transpiler to OCaml, a meta-circular evaluator and a partial evaluator. This project was done for the TIPE competitive examination at the end of classes prépas. More information can be found in the report, slides or technical slides (all in French).

Minetest

Minetest is a free, open-source voxel game engine. The engine is written in C++, using the Irrlicht engine, and content is added in Lua. I am a core developer of both Minetest and its default included game. I also contributed to a number of mods or additional content, some of them listed below.

Inside the Box (2016-2019), with sofar.

Inside the Box is a game for Minetest, where players have to solve small puzzles, and can create puzzles for other players on the server to play. There also is an official server, containing a lot of user-contributed content. See also the forum topics for the game and the server.

Technic (2013-2018), with the technic team.

Technic is a mod for Minetest, adding industrial-themed content, with electricity and a 3-tier system for progression. It has been developed by a large number of people over the years, and is among the most successful Minetest mods. Be sure to check the forum topic.

Pipeworks (2013-2018), with VanessaE and contributors.

Pipeworks is a mod for Minetest, adding pipes that can transport liquids and tubes that can transport items. I added the item transport layer and automation features on top of the impressive work VanessaE had previously done of creating very nice-looking pipes and tubes. The forum topic for this mod is located here.

Experimental mapgen (2013-2018), with sfan5.

Experimental mapgen, also named mg, is a custom Lua mapgen for Minetest, with Voronoi-based biome generation, ore veins and caves, and villages. The forum topic is here. After its release, Sokomine backported mg's village generation to work with all map generators and improved it further, yielding impressive results. Her work can be found here (forum topic).

Computers and programmable robots (2013-2015).

This mod provides programmable robots called "turtles", as in Logo. Although the robot was programmable in Lua in the early versions, this mod was later merged with my now obsolete forth_computer mod, adding computers and making both computers and turtles programmable using Forth. This was made by writing a fully Forth-83-compliant system for a virtual processor inspired by the 6502. Although some other languages could be implemented for that processor, none ever were, and the mod fell into abandon due to the lack of interest in the very low-level programming Forth represents. The almost empty forum topic can be found here.

Industrial Test (2013).

This was my first attempt at writing an industrial-themed mod. While having similarities to technic, it was not compatible with it and was eventually abandonned to work on technic instead, but its forum topic is still here. ElectricSolstice later forked this mod to create voltbuild, adding a number of extra features (forum topic).

Other projects

Debootstrapping the OCaml compiler (2019-2022), with Gabriel Scherer and JulienLepiller.

Implementation of an OCaml interpreter in a subset of OCaml named miniML, and of a compiler from miniML to OCaml bytecode in Scheme. Together, they allow to build the OCaml compiler from source only, as part of the Bootstrappable builds project. We published a paper (DOI, mirror) about it, and also presented this at the 10 Years of Guix event (slides).

Project Euler (2013-2019).

Project Euler is a website hosting small mathematics problems to be solved with the help of a computer, preferentially with programs running in less than one minute. At the time of writing, I solved all 685 problems available on Project Euler. Out of consideration for the website's philosophy, I will not publish my solutions here. However, you might be interested by my friend key.

Formally verified proof of Baire’s theorem (2019).

Statement and verification of Baire’s theorem that every locally compact Hausdorff space is a Baire space in Coq. The proof used was the proof available in the French Wikipedia article about Baire’s theorem.

Implementation of Wave Function Collapse with a focus on performance (2018), with Mathieu Fehr

Implementation of the Wave Function Collapse algorithm in C++. We improved the algorithm itself on some points, and also paid attention to low-level details such as cache management to get as much performance as we could. Backporting our optimisations gave a 20x speedup on the original implementation.

Formally verified proof of the law of quadratic reciprocity (2014).

Statement and verification of the law of quadratic reciprocity in Coq. The proof used was Eisenstein's proof, with combinatorial proofs of Wilson's theorem and Fermat's little theorem. This proof is listed in Freek Wiedijk's "Formalizing 100 Theorems" list.