TT Lite: a supercompiler for Martin-Löf's type theory

The paper describes the design and implementation of a certifying supercompiler TT Lite, which takes as input an input program and produces a residual program paired with a proof of the fact that the residual program is equivalent to the input one. As far as we can judge from the literature, this is the first implementation of a certifying supercompiler for a non-trivial higher-order functional language. The proof generated by TT Lite can be verified by a type checker which is independent from the supercompiler and is not based on supercompilation. This is essential in cases where the reliability of results obtained by supercompilation is of fundamental importance.