Добрый день всем!

Завтра, в четверг 24 июня в 15 часов, Илья Ключников расскажет о своей 
диссертационной работе по дальнейшему развитию суперкомпиляции на семинаре в 
Институте системного программирования РАН,  ул. Солженицына (бывш. Большая 
Коммунистическая), дом 25, http://ispras.ru/. См. ниже объявление с названием и 
аннотацией.

Практически все результаты Ильи опубликованы. На его сайте 
http://pat.keldysh.ru/~ilya/ выставлены pdf-файлы статей и даны ссылки на его 
суперкомпиляторы, которые запускаются на сервере через web-интерфейс, и на 
наборы примеров.

Речь идет о суперкомпиляции подмножества Хакеля. Подмножество не очень большое, 
но сам суперкомпилятор самый мощный из нам известных (включая ведущиеся сейчас 
работы в MS Research), хотя и весьма компактный. Его мощность основана на новых 
идеях, которые могут использоваться и в других методах анализа и преобразования 
программ.

В ИСП очень сильная команда по анализу программ, тестированию, верификации. 
Доложиться перед ними и выслушать критику - это самая сильная "апробация", 
которую может получить в Москве работа из нашей области. Я иду туда не просто 
"в свите" Ильи, но с настроением услышать интересное обсуждение. И вас 
приглашаем прийти с тем же. 

Пропускной режим там практически свободный. По предыдущим посещениям такой 
опыт: скажите, что на семинар, вахтер запишет в журнал, и подскажет, куда идти. 
Для уверенности можете прислать мне сообщение, что собираетесь, и я перешлю в 
ИПС списком.

Андрей Климов


Ключников Илья Григорьевич, ИПМ им. М.В. Келдыша РАН, 
http://pat.keldysh.ru/~ilya/

Выявление и доказательство свойств функциональных программ методами 
суперкомпиляции (по материалам кандидатской диссертации, научный руководитель 
С.А.Романенко)

1. Алгоритм суперкомпиляции для функций высших порядков. 
2. Использование суперкомпиляции для распознавания: 
   - эквивалентности выражений высшего порядка,
   - улучшающих лемм.
3. Улучшение асимптотики программ с помощью многоуровневой суперкомпиляции.
4. Применения.
   - Доказательство эквивалентности абстрактных машин.
   - Проверка корректности реализаций монад из стандартной библиотеки языка 
Haskell.

Ответить