Сведения о результатах публичной защиты (Трассирующая нормализация)

Протокол № 34.0б-51-1-4 заседания диссертационного совета Д 212.232.51 от 29 марта 2018 г. Состав диссертационного совета утвержден в количестве 21 человека, Присутствовали на заседании 1б человек: из них б докторов наук по специальности 05.13.11 — «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей» (физико-математические науки). Председательствующий: д. физ.-мат.наук, доцент Тулупьев Александр Львович. Присутствовали: д. физ.-мат.

наук Тулупьев Александр Львович, д. физ.-мат. наук Демьянович Юрий Казимирович, д. физ.-мат. наук Андрианов Сергей Николаевич, д. физ.-мат. наук Бурова Ирина Герасимовна, д. физ.-мат. наук Веремей Евгений Игоревич, д. физ.-мат. наук Граничнн Олег Николаевич, д. фнз.-мат. наук Ермаков Сергей Михайлович, д. физ.-мат. наук Корнеев Вадим Глебович, д. физ.-мат. наук Косовская Татьяна Матвеевна, д. физ.-мат. наук Кривулин Николай Кимович, д. тех. наук Лисс Александр Рудольфович, д. физ.-мат.

наук Мартыненко Борис Константинович, д. физ.- мат. наук Новиков Борис Асенович, д. пед. наук Поздняков Сергей Николаевич, д. физ.- мат. наук Романовский Иосиф Владимирович, д. физ.-мат. наук Терехов Андрей Николаевич. О4ициальные оппоненты по диссертации: доктор физико-математических наук, профессор Непейвода Николай Николаевич, кандидат физико-математических наук, доцент Миронов Андрей Михайлович. Ведущая организаиия: Федеральный исследовательский центр Институт прикладной математики им. М.В.

Келдыша Российской академии наук. Защиту диссертации Берез уна Даниила Андреевича на тему «' Грассирующая нормализация» на соискание ученой степени кандидата физико-математических наук по специальности 05.13.!1 — математическое н программное обеспечение вычислительных машин, комплексов и компьютерных сетей. Постановили: Диссертационная работа Березуна Д.А. является научно-квалификационной работой, которая содержит новые научные и практические результаты по актуальным вопросам лямбда-исчисления и теоретического программирования, имеет существенное значение для развития средств анализа программ н соответствует всем требованиям действующего Заместитель председателя диссертационного совета ~ульев Александр Львович Демьянович Юрий Казимирович Ученый секретарь совета «Положения о присуждении ученых степеней», предъявляемым к диссертациям на соискание ученой степени кандидата наук, в том числе п.9 (абзац 2).

На основании результатов тайного голосования членов диссертационного совета (за — Л, против — '~, недействительных бюллетеней — ~~ ) диссертационный совет принял решение присудить Березуну Д.А. ученую степень кандидата физико-математических наук по специальности 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей.

ЗАКЛЮЧЕНИЕ ДИССЕРТАЦИОННОГО СОВЕТА Д 212.232.51 НА БАЗЕ ФЕДЕРАЛЬНОГО ГОСУДАРСТВЕННОГО БЮДЖЕТНОГО ОБРАЗОВАТЕЛЬНОГО УЧРЕЖДЕНИЯ ВЫСШЕГО ОБРАЗОВАНИЯ «САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ», ПРАВИТЕЛЬСТВО РФ, ПО ДИССЕРТАЦИИ НА СОИСКАНИЕ УЧЕНОЙ СТЕПЕНИ КАНДИДАТА НАУК аттестационное дело № решение диссертационного совета от 29 марта 2018 г. № 34.0б.51-1-4 О присуждении Березуну Даниилу Андреевичу, гражданину Российской Федерации, ученой степени кандидата физико-математических наук. Диссертация «Трассирующая нормализация» по специальности 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей принята к защите 28 декабря 2017 года, протокол Х 34.0б-51-1-4 диссертационным советом Д 212.232.51 на базе Федерального государственного бюджетного образовательного учреждения высшего образования «Санкт-Петербургский государственный университет», Правительство РФ, 199034, г. Санкт-Петербург, Университетская наб., д.

7-9, приказ 248/нк от 15.05.2014 г. Соискатель Березун Даниил Андреевич 1992 года рождения. В 2014 году соискатель окончил Федеральное государственное образовательное учреждение высшего профессионального образования «Санкт-Петербургский государственный университет» по специальности «Математическое обеспечение и администрирование информационных систем», является аспирантом Федерального государственного бюджетного образовательного учреждения высшего образования «Санкт-Петербургский государственный университет», в настоящее время не работает.

Диссертация выполнена на кафедре системного программирования Федерального государственного бюджетного образовательного учреждения высшего образования «Санкт-Петербургский государственный университет», Правительство РФ. Научный руководитель — доктор технических наук Кознов Дмитрий Владимирович, Федеральное государственное образовательное учреждение высшего профессионального образования «Санкт-Петербургский государственный университет», кафедра системного программирования, профессор.

Официальные оппоненты: Непейвода Николай Николаевич, доктор физико-математических наук, профессор, Федеральное государственное бюджетное учреждение науки Институт программных систем имени А.К. Айламазяна Российской академии наук, отдел инструментального и прикладного программного обеспечения, главный научный сотрудник; Миронов Андрей Михайлович, кандидат физико-математических наук, Федеральное государственное бюджетное образовательное учреждение высшего образования «Московский государственный университет имени М.В.Ломоносова», кафедра интеллектуальных систем, доцент дали положительные отзывы на диссертацию. Ведущая организация Федеральное государственное учреждение «Федеральный исследовательский центр Институт прикладной математики им. М.В.

Келдыша Российской академии наук» (ИПМ им. М.В. Келдыша РАН), в своем положительном отзыве, подписанном ведущим научным сотрудником, кандидатом физико-математических наук (специальность 01.01.10 — математическое обеспечение вычислительных машин и систем) С.А. Романенко и утвержденном директором ИПМ им. М.В.

Келдыша РАН А.И. Аптекаревым, указала, что диссертационная работа Березуна Д.А. является законченной научно-квалификационной работой, которая содержит новые научные и практические результаты, связанные с решением актуальной задачи, соответствует паспорту специальности 05.13.11, а ее автор заслуживает присуждения ученой степени кандидата физикоматематических наук по специальности 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей. Соискатель имеет 5 опубликованных работ, все — по теме диссертации, в том числе 2 работы опубликованы в рецензируемых научных изданиях из перечня российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук и 2 работы опубликованы в изданиях, индексируемых в международных базах Ясорпз и %еЬ оЕ Кс1епсе.

В диссертации отсутствуют недостоверные сведения о работах, опубликованных соискателем. В опубликованных работах соискателя общим объемом б4 страницы, исследованы вопросы, связанные с нормализацией термов в нетипизированном лямбда-исчислении, разработан алгоритм трассирующей нормализации для нетипизированного лямбда-исчисления, соответствующий нормальному порядку редукции, корректность предложенного алгоритма доказана, алгоритм адаптирован для других, отличных от нормального порядка, стратегий вычислений, предложен новый метод компиляции функциональных языков программирования в низкоуровневое представление, а также разработана пилотная реализация предложенных алгоритма и подхода, сформулированы рекомендации по применению результатов диссертационного исследования в индустрии и научных исследованиях.

Работы выполнены автором лично или при его активном непосредственном участии. В диссертации отсутствуют недостоверные сведения о работах, опубликованных соискателем. Наиболее значительные научные работы по теме диссертации (в них соискателю принадлежит разработка и формализация метода трассирующей нормализации, реализация предложенных семантических преобразований, идея и формализация метода трассирующей нормализации для языка РСГ, а также формализация и доказательство корректности полной головной линейной редукции и предложенного алгоритма трассирующей нормализации, соавторы предложили схему представления нормализирующей процедуры, описали применение частичных вычислений к процедуре нормализации с целью компиляции термов лямбда-исчисления, сформулировали направления дальнейших исследований): 1.

Березун, Д.А. Полная головная линейная редукция / Д.А. Березун // НТВ СПбГПУ. Информатика, Телекоммуникации. Управление. — 2017. — № 3.— С. 59-82. 2. Березун, Д.А. Трассирующая нормализация нетипизированного лямбдаисчисления / Д.А. Березун // Известия вузов. Северо-Кавказский регион. Технические науки. — 2017. — № 4. — С. 5 — 12. 3. Вегекип, Р.А. Сотр!!1пя 1!пгуред 1.агпЬда Са!си!пз го 1.о~чег-Ьече! Соде Ьу Оапге Бе|пап!!сз апд Рагйа1 Еча!пайоп (1пч!гед рарег) / О.А. Вегекип, Ь!.О.

1опез // Ргосеед1пяз о1 !Ье 2017 АСМ 81бР1.АЬ! ЖогКзЬор оп Рагба! Еча!иаг1оп апд Ргоягагп Мап1ри!аг!оп (РЕРМ 2017). АСМ, Ь!еч Уог!с, Ь!У, 1)БА. — 2017. — С. 1 — 11. На автореферат поступили отзывы, все отзывы положительные: 1. От доктора технических наук, профессора кафедры «Прикладная математика» Института прикладной математики и механики федерального государственного автономного образовательного учреждения высшего образования «Санкт-Петербургский политехнический университет Петра Великого» Новикова Федора Александровича.

В качестве замечания указана необходимость уточнения термина «система переходов» ввиду его перегруженности в современной науке. 2. От кандидата технических наук, доцента, заведующего кафедрой «Компьютерных систем и программных технологий» Института компьютерных наук и технологий федерального государственного автономного образовательного учреждения высшего образования «СанктПетербургский политехнический университет Петра Великого» Ицыксона Владимира Михайловича.

Указаны нижеследующие замечания: 1. Представляется не очень удачной формулировка темы диссертации, так как трассирующей нормализацией занимались и до автора. Основной вклад автора — применение трассирующей нормализации к Тьюринг-полным языкам. Это и следовало бы включить в название. 2. Несмотря на то, что в работе уделено определенное внимание практическим аспектам применения разработанных алгоритмов, полагаю, что конкретизация применения результатов на практике раскрыта недостаточно полно.