Головная страница ИПМ Библиотеки, издания  •  Поиск публикаций  English 
Публикация

Препринт ИПМ № 73, Москва, 2013 г.
Авторы: Ключников И. Г., Романенко С. А.
TT Lite: суперкомпилятор для теории типов Мартина-Лёфа
Аннотация:
Описывается структура и реализация сертифицирующего суперкомпилятора TT Lite, преобразующего исходную программу в пару, содержащую остаточную программу и доказательство того, что остаточная программа эквивалентна исходной. Насколько можно судить по существующим публикациям, сертифицирующая суперкомпиляция для нетривиального функционального языка высшего порядка реализована впервые. Доказательства, порождаемые суперкомпилятором TT Lite могут быть верифицированы проверяльщиком типов, который независим от суперкомпилятора и не основан на суперкомпиляции. Это существенно в ситуациях, когда решающее значение имеет надежность результатов, полученных с помощью суперкомпиляции.
Ключевые слова:
Суперкомпиляция, теория типов, верификация.
Язык публикации: английский,  страниц: 28
Направление исследований:
Программирование, параллельные вычисления, мультимедиа
Полный текст на английском языке:
Статистика просмотров (обновляется раз в сутки):
за последние 30 дней — 0 (-1), всего с 01.09.2019 — 3
Сведения об авторах:
  • Ключников Илья Григорьевич,  ,  ИПМ им. М.В. Келдыша РАН
  • Романенко Сергей Анатольевич,  orcid.org/0000-0002-2971-9647,  ИПМ им. М.В. Келдыша РАН