KIAM Main page Web Library  •  Publication Search   

KIAM Preprint  73, Moscow, 2013
Authors: Klyuchnikov I. G., Romanenko S.A.
TT Lite: a supercompiler for Martin-Löfs 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.
Supercompilation, type theory, verification.
Publication language: english, pages: 28
Research direction:
Programming, parallel computing, multimedia
Source text: