In dependently-typed functional programming languages that allow general
recursion, programs used as proofs must be evaluated to retain type soundness. As a result,
programmers must make a trade-off between performance and safety. To address
this problem, we propose System DE, an explicitly-typed, moded core calculus
that supports termination tracking and equality reflection. Programmers can
write inductive proofs about potentially diverging programs in a logical
sublanguage and reflect those proofs to the type checker, while knowing that
such proofs will be erased by the compiler before execution. A key
feature of System DE is its use of modes for both termination and relevance
tracking, which not only simplifies the design but also leaves it
open for future extension. System DE is suitable for use in the Glasgow
Haskell Compiler, but could serve as the basis for any general purpose
dependently-typed language.