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.
The first example in the Verse paper appears problematic because "there's no scrutinee." But in the Verse terms obtained by translation from $P$, there is not obviously a scrutinee. So what concept about or property of Verse terms stands in for "there is a scrutinee?"
The first example in the Verse paper appears problematic because "there's no scrutinee." But in the Verse terms obtained by translation from $P$, there is not obviously a scrutinee. So what concept about or property of Verse terms stands in for "there is a scrutinee?"