for random projects that have nowhere else to go.

• I built lean-symb out of frustration at the fact that there was nothing of the sort out there. If you’re here, it might be of interest or use to you! do have a look.
• Over the course of my life, I wrote a bunch of personal utilities in a variety of languages and technologies for very specific use cases I had. I learned a lot, but I wouldn’t call that code particularly useful. It’s kept on my github for archival purposes.

As a semester research project under Prof. Thomas Bourgeat, I tackled the formalization of the results published as The 2-Dimensional Constraint Loop Problem is Decidable (2024) by Guilmant et al. The formalization was carried out in Lean, making heavy use of Mathlib for the foundational mathematical results.

The project was a lot of fun, despite the heavy reliance on mathematics that were far above my puching weight. In the end, all of the machinery was formalized, and good progress was carried out on the main result in the 1D case. The 2D case follows a similar argument, and is deferred :(.

The project’s achievements, limitations, and main conclusions can be found in the presentation for a quick overview, and in the report.

For CS428 - Interactive Theorem Proving, we implemented Steele, a verified decompilation framework for WebAssembly. We lift a WebAssembly module to a higher-level representation, FLInt, on which decompilation passes introduce new abstractions and deobfuscations. Every pass is verified, ensuring the correctness of the whole decompilation process. We implemented and verified the lifting pass, as well as a proof of concept pass introducing pointer dereferencing.

The project was a good introduction to simulation relations, and despite the (many) difficulties, it was a good first project to learn Rocq and theorem proving in general. The code can be found on codeberg, along with the PDF report.

Beyond more work on the projects here mentioned, there are multiple projects in the pipeline, including:

I’m currently reading on the formalization and implementation of higher-order calculi in Lean: the long term goal is implementing a dependently-typed programming language, with a simple tactic mode, while documenting the journey in a “theorem proving from scratch” series of reports.

I’m also interested in formalizing the Verse calculus, a core calculus for functional logic programming. Its syntax and semantics are described in the preprint paper, which looks really interesting, and probably a lot of fun to formalize.