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

Описывается структура и реализация сертифицирующего суперкомпилятора TT Lite, преобразующего исходную программу в пару, содержащую остаточную программу и доказательство того, что остаточная программа эквивалентна исходной. Насколько можно судить по существующим публикациям, сертифицирующая суперкомпиляция для нетривиального функционального языка высшего порядка реализована впервые. Доказательства, порождаемые суперкомпилятором TT Lite могут быть верифицированы проверяльщиком типов, который независим от суперкомпилятора и не основан на суперкомпиляции. Это существенно в ситуациях, когда решающее значение имеет надежность результатов, полученных с помощью суперкомпиляции.