Сведения о результатах публичной защиты (1150916), страница 2
Текст из файла (страница 2)
3. В тексте реферата имеются грамматические и стилистические ошибки. От кандидата физико-математических наук, разработчика программного обеспечения компании «Расе ЬооК 13К» (Лондон) Ключникова Ильи Григорьевича. В качестве замечания предложено рассмотреть плюсы и минусы получаемого в результате предложенного метода компиляции низкоуровневого представления с практической точки зрения. Ответы на замечания в отзывах на автореферат даны в ходе защиты. От доктора технических наук Штейнберга Бориса Яковлевича, заведующего кафедрой алгебры и дискретной математики Института математики, механики и компьютерных наук им. И.И.Воровича Южного федерального университета. Отзыв замечаний не содержит.
От кандидата физико-математических наук, доцента кафедры компьютерных технологий федерального государственного автономного образовательного учреждения высшего образования «СанктПетербургский национальный исследовательский университет информационных технологий, механики и оптики» ~Университет ИТМО) Андрея Александровича Фильченкова. Отзыв замечаний не содержит.
Выбор ведущей организации обосновывается тем, что она имеет значительный опыт исследований, непосредственно соответствующих тематике данной диссертационной работы и способна определить научную и практическую ценность диссертации. Выбор в качестве официального оппонента Непейвода Н.Н. обусловлен тем, что он является ведущим ученым РФ в данной области, имеет непосредственное отношение к теме и предмету диссертационного исследования, является автором многочисленных публикаций. Выбор в качестве официального оппонента Миронова А.М. обусловлен тем, что он является признанным в России экспертом в области теоретического программирования и информатики, активно публикуется и выступает с докладами в этих областях.
Диссертационный совет отмечает, что на основании выполненных соискателем исследований: разработано обобщение трассирующей нормализации для Тьюринг-полных моделей вычислений с выполнением свойства полукомпозициональности для нормального порядка вычислений; предложен алгоритм трассирующей нормализации; доказана корректность данного алгоритма; введено понятие полной головной линейной редукции, обобщающее известное понятие головной линейной редукции. Теоретическая значимость исследования обоснована тем, что: доказана теорема о том, что трассирующая нормализация для бестипового лямбда-исчисления, действительно является процедурой нормализации,' использована формальная модель системы переходов; изложены идеи о применении трассирующей нормализации к другим стратегиям вычислений, отличным от нормального порядка; изучены связи трассирующей нормализации с частичными вычислениями и проекциями Футамуры — Ершова — Турчина; проведена модернизация модели головной линейной редукции, позволившая выполнить доказательство основного теоретического результата работы.
Значение полученных соискателем результатов исследования для практики подтверждается тем„что: разработан новый метод компиляции функциональных языков программирования в низкоуровневое представление путем специализации представленного алгоритма трассирующей нормализации на входной терм; создана реализация данного метода; представлены методические рекомендации по специализации процедуры нормализации для различных функциональных языков программирования.
Результаты работы рекомендуются к использованию в Институте программных систем им. А.К.Айламазяна РАН, Московском государственном университете им. М.В.Ломоносова, Санкт-Петербургском государственном университете, Институте прикладной математики им. М.В. Келдыша РАН, Институте системного программирования РАН, н могут найти применение при реализации языков программирования, а также программного инструментария для оптимизации и верификации программ. Оценка достоверности результатов исследования выявила, что: теория построена на адекватном математическом аппарате и согласуется с более ранними результатами; идея базируется на обобщении линейной головной редукции, а также на анализе алгоритмов специализации средств обработки программ; использованы аппарат лямбда-исчисления и частичные вычисления ~в том числе, проекции Футамуры-Ершова-Турчина); установлено, что алгоритм трассирующей нормализации является процедурой нормализации и обладает свойством полукомпозициональности, что открывает интересные перспективы по применению полученных результатов в частичных вычислениях и теоретическом программировании; использованы последние результаты в области лямбда-исчисления и теоретического программирования.
Личный вклад соискателя состоит в разработке и формализации метода трассирующей нормализации, реализации предложенных семантических преобразований, формализации трассирующей нормализации для языка РСГ, а также формализации и доказательстве корректности полной головной линейной редукции и предложенного алгоритма трассирующей нормализации, создании и реализации метода компиляции функциональных языков; апробации работы на различных всероссийских и международных конференциях и семинарах; подготовке основных публикаций по выполненной работе.
Диссертационная работа Березуна Д.А. является заверше*иной научно- квалификационной работой, которая содержит новые научные и практические результаты по актуальным вопросам лямбда-исчисления и теоретического программирования, имеет существенное значение для развития средств анализа программ и соответствует всем требованиям действующего «Положения о присуждении ученых степеней», предъявляемым к диссертациям на соискание ученой степени кандидата наук, в том числе п.9 (абзац 2). На заседании 29 марта 2018 года диссертационный совет принял решение присудить Березуну Д.А. ученую степень кандидата физикоматематических наук. При проведении тайного голосования диссертационный совет в количестве 1б человек„ из них б докторов наук по специальности О5.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей (отрасль физико-математические науки), участвовавших в заседании, из 21 человека, входящего в состав совета, проголосовали: за '~~, против '~, недействительных бюллетеней С~, Заместитель председателя в Александр Львович диссертационного совета '-, Демьянович Юрий Казимирович Ученый секретарь диссертационного совета 29 марта 2018 года .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
