Отзыв на автореферат 5 (Трассирующая нормализация)

отзыв на автореферат диссертационной работы Березуна Даниила Андреевича на тему «Трассирующая нормализация», представленную на соискание ученой степени кандидата физико-математических наук по специальности 05.13.11— «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей» Актуальность темы диссертации Березуна Даниила Андреевича обусловлена тесной связью с реальными проблемами, возникающими при разработке и реализации математичесюго и программного обеспечения, в том числе с такими как формальное определение семантики языюв программирования, верификация и доказательство правильности программ. Результаты, полученные в диссертации, могут найти применение при создании программного инструментария для работы с современными практическими системами программирования. Поэтому актуальность и практическая значимость диссертационной работы Березуна Д.А.

не вызывает сомнений. Научная новизна диссертации бросается в глаза. Березиным Д.А. получен ряд существенно новых результатов, обобщающих и расширяющих ранее известные результаты в этой области. В том числе предложена модель полной головной линейной редукции, обобщающей модель головной линейной редукции и применимой для нетипизированного лямбда-исчисления'„ построен алгоритм трассирующей нормализации, который вычисляет нормализованный терм без изменения исходного терма; показана возможность юмпиляции термов лямбда-исчисления посредством специализации алгоритма нормализации по отношению к терму.

Достоверность основных положений подтверждается широкой апробацией полученных результатов на представительных конференциях и публикацией пяти научных работ, зарегистрированных в РИНЦ. При этом две единоличные статьи изданы в журналах из "Перечня рецензируемых научных изданий, в которых должны быть опубликованы основные научные результаты диссертаций на соискание учйной степени кандидата наук, на соискание ученой степени доктора наук", и две статьи опубликованы в изданиях, входящих в базы цитирования Ясорпз и %еЬ оГ 3с~епсе.

Замечание относится сюрее к форме представления результатов в автореферате, нежели к самой работе. Автор указывает, что для формализации моделей и доказательства корректности использовались системы переходов. Однако в настоящее время термином «система переходов» разные авторы называют похожие, но все-таки различные формализмы, в том числе, например, с действиями на переходах. В автореферате не указывается, какой именно формализм использовался. Из юнтекста можно предположить, что подразумевается оригинальная система Келлера, но лучше было бы указать это явно. Заключение. Диссертационная работа Березуна Д.А.

на тему «Трассирующая нормализация» является законченной научно-квалификационной работой, содержит новые научные и практические результаты, связанные с решением актуальной задачи, имеющей большое значение для развития методов разработки и реализации математического и программного обеспечения вычислительных машин, комплексов и компьютерных сетей. Автореферат диссертационной работы соответствует паспорту специальности 05.13.11, а автор заслуживает присуждения учбной степени кандидата физико-математических наук по специальности 05.13.11 — «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей». Доктор технических наук (специальность 05.13.11 — «Математическое и программное обеспечение вычислительных машин, комплексов н компьютерных сетей), профессор кафедры «Прикладная математика» Института прикладной математики и механики Санкт-Петербургского политехнического университета Петра Великого 195251, Санкт-Петербург, Политехническая, 29 Сайт: Ыг://в им.з ЬзГн.ги/ Тел.: +7 921 574-79-44 Эл.

почта: ГедогпояЕоч51 а гпа11.сот 23.03.2018 едор Александрович Новиков УД ~ 8«лга» Ф,~" .