Code and proofs for Verse-ML, an equation-style sub-ml language. Part of an undergraduate senior thesis with Norman Ramsey, Milod Kazerounian, and Roger Burtonpatel.
Done at the board today. Key idea: parameterize the tree with a type variable. The parameterization separates "act of deciding" from "action to take once decision has been made."