Software

KReMLin

“K&R meets ML” (pun courtesy of Graydon).

KReMLin implements the compilation scheme of Low*, i.e. it translates F* programs that are valid Low* into readable C. Readable C is of particular importance for software practicioners (e.g. Mozilla) to read, understand and trust our code. KReMLin extends the Low* theory, and will compile data types & pattern matches, monomorphize polymorphic functions, eliminate unused arguments, simplify data types, and apply many more passes to enhance the quality of the generated C code. Importantly, KReMLin has a set of options that make up a mini DSL to get rid of abstraction and modularity, in favor of tight, compact self-contained C files, a must-have in an actual software project.

KReMLin is open-source, and lives on GitHub.

Verified software

• I am driving the EverCrypt project, in collaboration with INRIA and CMU and a large subset of Project Everest members.
• I am a core contributor to HACL*.
• I also contribute to miTLS.

Thunderbird addons

I was a core contributor, peer and module owner of Thunderbird for several years. During this time, I contributed numerous patches to Thunderbird, along with several add-ons. Amazingly, with the help of contributors, these addons have been running for nearly ten years now.

• Thunderbird Conversations offers a conversation view for Thunderbird. The addon is a large piece of code and replaces the message reader in Thunderbird. Thunderbird Conversations is on GitHub, and is chiefly maintained by Mark Banner nowadays.
• Thunderbird Stdlib was an attempt at a standard library for addons, providing reference implementations for complicated tasks (e.g. assemble and send an HTML email).
• Manually Sort Folders is now the most popular addon. The name is self-explanatory, and the addon is available on GitHub.
• Latex It! runs Latex on your computer, and transforms $x$ in your email body into the corresponding rendered image. The addon is also on GitHub.

BBC micro:bit hacking

I did a few fun hardware projects with the BBC micro:bit. Here’s some cursory instructions for creating a clock / temperature display; you can also live-stream sensor data from the micro:bit to your javascript web page over usb (very rough instructions).

Misc.

• The Mezzo type-checker, including some custom solving strategies for framing & inference. My dissertation has all the details.
• I maintained the OCaml Installer for Windows for too long (2011-2016). Now, please use fdopen’s distribution as it is much better.
• A stylesheet for OCamldoc. See an OCaml module, and the sample documentation.
• A stylesheet for LaTeX documents. It gives a very condensed, two-column layout for article document classes. It also adds a \part command that gives the book-like heading seen in my reports (see here for an example). The heading was initially an attempt to reproduce the style of the French LaTeX pour l’impatient book.
• An IRC client written in PHP-GTk. When I was in high school, I would stay up all night during summer break and code like a madman. Those were the days.