Projects

These first few projects are close to an actual product rather than a package or something else:

Molasses

Molasses is a tool for converting SML programs that use different Standard ML compilers so that they are cross-compatiable. More specifically, Molasses takes programs using MLB (ML Basis) files which are primarily used by the MLton compiler and translates them into CM (compilation manager) files which are used by the SML/NJ compiler.

Doing this has a number of benefits. MLton generally produces faster executables but SML/NJ has very fast compilation times and can be debugged in a REPL. MLB files also allow for top-level expression and infix declarations which allows programs to define common operators once and they can be used everywhere. Also, Molasses uses a parser which produces significantly more readable error messages.

Currently, this project is in a stable condition. In the future I may add support for deviations in the standard libraries, potentially allowing Parallel ML code to be ran in SML/NJ but I don't plan on doing this anytime soon.

C0deine

C0deine is a C0 compiler written in Lean and currently outputs WebAssembly. The ultimate goal is to verify the correctness of the output, meaning if you write a C0 program, the compiled WebAssembly program is guarenteed to have the same behaviour.

This project has been my primary focus and uses some of the other libraries I've written below. One of the primary features of C0 is that it allows the ability to reason about C code (through the use of contracts). Currently, that reasoning is done on pen and paper. Having C0 formalised in Lean allows creates a framework which could potentially allow for the reasoning about C code within Lean itself. This means that rather than relying the proof of correctness that are written down, they could be machine checked.

SML Help

SML Help is a resource for learning Standard ML which I've written a couple of pages for and help maintain (among a number of people). If you want to contribute or need a PR reviewed or approved please reach out!

Lean Packages

These are smaller packages that I've written/help maintain that might be useful for writing Lean:

  • Numbers implements arbitrary bit-length integers (both signed and unsigned) as well as a bunch of operations. It also includes a LEB128 encoder/decoder. Currently intended to match the WebAssembly specification but certainly could be extended.
  • DateTime a package that has utilities for reasoning about dates and times (inspired by similar projects in other programming languages).
  • Lean-Wasm a currently incomplete, formalisation of the WebAssembly specification in Lean. Also included is notation for WASM. What this means is that you can write WebAssembly (in text format) and embed them within Lean programs.
  • Control Flow is a verified implementation of control flow graphs as well as proofs about them and other graph theory results. This is primarily used by C0deine, but could be useful in other places hence why it is a separate package.
  • Lean2Wasm is a utility/wrapper that takes compiled Lean programs and translates them into WebAssembly (by interfacing with emscripten).

    • Demos/Proofs-of-Concepts

  • Pauline - This is an embedding of a subset of Standard ML into Lean and which can then be used to write proofs about the code. This would be really cool if this was developed further, but I was mostly working on it to get an idea of how to do something similar for C0. I assume something of this nature will eventually be made, even if it is not implemented in Lean.
  • Inference Rules - This is a tool for converting inductive types in Lean into LaTeX'd inference rules. Currently it is somewhat hacked together, so it is still within the C0deine repository. I intend to port this into its own package at some point.