|
Preprints of the Keldysh Institute of Applied Mathematics, 2013, 073, 28 pp.
(Mi ipmp1823)
|
|
|
|
TT Lite: a supercompiler for Martin-Löf's type theory
Ilya G. Klyuchnikov, Sergei A. Romanenko
Abstract:
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.
Citation:
Ilya G. Klyuchnikov, Sergei A. Romanenko, “TT Lite: a supercompiler for Martin-Löf's type theory”, Keldysh Institute preprints, 2013, 073, 28 pp.
Linking options:
https://www.mathnet.ru/eng/ipmp1823 https://www.mathnet.ru/eng/ipmp/y2013/p73
|
|