ANF preserves dependent types up to extensional equality

Paulette Koronkevich
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 no guarantees after compiling, nor when linking after compilation. Type-preserving compilers preserve guarantees encoded in types, then use type checking to verify compiled code and ensure safe linking with external code. Unfortunately, standard compiler passes do not preserve the dependent typing of commonly used (intensional) type theories. This is...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.