A formalization of (a subset of) SML semantics in Lean.
Called "Pauline" because it sounds like a mashup of "Polly", the course mascot of 150 and "Lean".
This is held together with zipties and hotglue. A lot of it would need to be re-written to get into a usable state.