“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.
- 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.
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
- 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
articledocument classes. It also adds a
\partcommand 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.