Provable Standard ML Programs in Lean - A subset of Standard ML, including dynamic semantics, is implemented in Lean 4. Using a variety of newly implemented tactics, this allows for writing machine checkable proofs about SML code similarly to how one would on paper.
