KIAM Main page Web Library  •  Publication Searh   

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
English source text:
List of publications citation:
Export link to publication in format:   RIS    BibTeX
View statistics (updated once a day)
over the last 30 days 1 (+1), total hit from 01.09.2019 102
About authors:
  • Klyuchnikov Ilya Grigor'evich,  KIAM RAS
  • Romanenko Sergei Anatolievich, RAS