Identify and formalize K-normal form for case expressions

rogerburtonpatel / vml

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.

5 stars 0 forks source link

Identify and formalize K-normal form for case expressions #14

Closed nrnrnr closed 7 months ago

nrnrnr commented 8 months ago

The key property of KNF is that if a value resides in a register at run time, it has a name in the source code:

Propose a KNF for case expressions.
Show that it has the key property.

nrnrnr commented 7 months ago

Done at the board today.