open.library.ubc.ca
ANF preserves dependent types up to extensional equality
A growing number of programmers use dependently typed languages such as Coq to machine-verify important properties of high-assurance software. However, existing compilers for these languages provide...
