Ilya G. Klyuchnikov, Sergei A. Romanenko. TT Lite: a supercompiler for Martin-Löf’s type theory. Keldysh Institute Preprints, (73), 2013. - 28 p.
URL: http://library.keldysh.ru/preprint.asp?lg=e&id=2013-73 Scala code: https://github.com/ilya-klyuchnikov/ttlite The paper describes the design and implementation of a certifying supercompiler TT Lite, which takes as input a 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. И.Г. Ключников, С.А. Романенко. TT Lite: суперкомпилятор для теории типов Мартина-Лёфа. Описывается структура и реализация сертифицирующего суперкомпилятора TT Lite, преобразующего исходную программу в пару, содержащую остаточную программу и доказательство того, что остаточная программа эквивалентна исходной. Насколько можно судить по существующим публикациям, сертифицирующая суперкомпиляция для нетривиального функционального языка высшего порядка реализована впервые. Доказательства, порождаемые суперкомпилятором TT Lite могут быть верифицированы проверяльщиком типов, который независим от суперкомпилятора и не основан на суперкомпиляции. Это существенно в ситуациях, когда решающее значение имеет надежность результатов, полученных с помощью суперкомпиляции.
