Выписка из протокола заседания диссертационного совета (Трассирующая нормализация)

ВЫПИСКА 34.06-51-2-3 из протокола № 34.06-51-1-4 заседания диссертационного совета Д 212.232.51 на базе Санкт-Петербургского государственного университета от «28» декабря 2017 года Подлинник протокола находится в делах диссертационного совета Санкт-Петербургского государственного университета Присутствовали: 14 (из 21) членов диссертационного совета: д. физ.-мат.

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

физ.-мат. наук, доцент Косовская Татьяна Матвеевна, д. тех. наук, профессор Лисс Александр Рудольфович, д. физ.-мат. наук, доцент Мартыненко Борис Константинович, д. ф~в.-мат, наук, профессор Новиков Борис Асеновнч, д. физ.-мат. наук, профессор Романовский Иосиф Владимирович, д. физ.-мат. наук, профессор Терехов Андрей Николаевич. Принятие к защите диссертации Березуна Даниила Андреевича на тему «Трассирующая нормализация», представленной к защите на соискание ученой степени кандидата физикоматематических наук по специальности 05.13,11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей, утверждение официальных оппонентов и ведущей организации.

ВЫСТУПИЛИ доктор физ.-мат. наук, профессор Демьянович Юрий Казимирович— председатель экспертной комиссии совета в составе доктора физ.-мат. наук профессора Баранова Сергея Николаевича, доктора физ.-мат. наук профессора Романовского Иосифа Владимировича - зачитал заключение комиссии о диссертации Березуна Даниила Андреевича на тему' «Трассирующая нормализация» по специальности 05.13.11— математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей, выполненной в Санкт-Петербургском государственном университете.

ПОСТАНОВИЛИ: 1. Утвердить заключение комиссии диссертационного совета по решению вопроса о соответствии диссертации Березуна Даниила Андреевича на тему «Трассирующая нормализация» профилю диссертационного совета Д 212.232.51 и заявленной теме. Тема и содержание диссертации Березуна Д.А. соответствует по области исследований указанным в паспорте специальности 05.13.11 "Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей" (отрасль физико-математические науки) пункту пунктам 1 (Методы, модели и алгоритмы проектирования и анализа программ и программных систем, их эквивалентных преобразований, верификации и тестирования) и 2 (Языки программирования и системы программирования, семантика программ).

2. Принять к сведению заключение комиссии диссертационного совета Д 212.232.51 о том, что: ° Обоснованность и достоверность полученных результатов подтверждается публикациями по материалам диссертации (5 публикаций), включая 2 статьи в журнале, входящем в Перечень рецензируемых научных изданий, 2 работы в изданиях, входящих в международную реферативную базу Бсорпя. ° Практическая значимость результатов диссертационного исследования заключается в предложении нового подхода к автоматической генерации компиляторов функциональных языков на основе описания семантики (БетапйсзИгесгед Сошр11ег Оепегаг)оп).

° Диссертация прошла проверку в системе В1аскЬоап1 на предмет выявления объема текстовых совпадений между текстом диссертации и источниками, авторство которых установлено, для рассмотрения диссертации как оригинальной научно- квалификационной работы.

Текстовых совпадений 9%. Диссертация Березуна Даниила Андреевича может считаться полностью оригинальной авторской научной работой. 3. Принять диссертацию на соискание ученой степени кандидата физико-математических наук к защите по специальности 05.13.11 "Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей" (отрасль физикоматематические науки).

4. Назначить официальных оппонентов, известных в области физико-математических наук ученых, имеющих публикации в сфере исследований математического и программного обеспечения вычислительных машин, комплексов и компьютерных сетей и давших на это свое согласие: Фамилии, Ими, Отчество ченое ванне ченаи епень Должность и место работы, адрес епейвода Николай доктор профессор нколаевнч физикоматематичес ких наук Главный научный сотрудник отдела инструментального и прикладного программного обеспечения федерального государственного бюджетного ч еждения на ки Таким образом, установлено, что диссертация Березуна Д.А. соответствует требованиям текущих редакций постановления "О порядке присуждения ученых степеней" и "Т1оложение о совете по защите диссертаций...".

<Институт программных систем имен .К. Айламазяна Российской академии наук», 152021, Ярославская обл., Переславскнй район, с. Веськово, ул. Пе аПе вого,д.4а Доцент кафедры математической теории интеллектуальных систем еханико-математического факультет федерального государственного бюджетного учреждения высшего образования "Московский государственный университет имени М.В. Ломоносова", 119991, г. Москва, Ленинские Го ы, д. 1 Доцент пронов Андрей ихайловпч кандидат физико- математичес ких наук 6. Предполагаемая дата защиты — 29 марта 2018 года. 7. Утвердить список организаций и лиц рассылки автореферата.

8, Разрешить опубликовать автореферат на правах рукописи. Решенно днссертапнонцого совета по данному вопросу принято единогласно. Председатель диссертационного совета Н.К. Косовский Ученый секретарь диссертационного совета Ю.К. Демьянович 5. Назначить ведущую организацию, широко известную своими достижениями в физикоматематической и технической отраслях науки и способную определить научную и практическую ценность диссертации и давшую на зто свое согласие, федеральное государственное учреждение «Федеральный исследовательский центр Институт прикладной математики им. М.В.

Келдыша Российской академии наук», 125047, г. Москва, Миусская пл., д.4. ЗАКЛЮЧЕНИЕ экспертной комиссии диссертационного совета Д 212.232.5 ! по кандидатской диссертации Березуна Даниила Андреевич на тему «Трассирующая нормализация» Комиссия диссертационного совета Д 212.232.51 на соискание ученой степени кандидата физико-математических наук в составе: председателя — доктора физико-математических наук, профессора Демьяновича Юрия Казимировича и членов комиссии: доктора физико-математических наук„профессора Баранова Сергея Николаевича, доктора физико-математических паук, профессора Романовского Иосифа Владимировича на основании ознакомления с кандидатской диссертацией Бсрсзуна Даниила Андреевича н состоявшегося обсуждения приняла следующее заключение. Диссертация Березуна Даниила Андреевич «Трассирующая нормализациям представлена на соискание ученой степени кандидата физико-математических наук по специальности 05.13.11 — «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей».

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

Работа Березуна Даниила Андреевича посвятцена расширению трассируюшей нормализации с типизированного на нетнпизированное лямбдаисчисление, а также адаптации предложенного алгоритма нормализации для различных стратегий вычислений. Актуальность тематики обеспечена последними результатами в этой области !работы Л.Онга и В. Блюма), развитием денотационных и игровых сем анти к языков программирования„а также необходимостью средств автоматизации обработки функциональных языков. Также актуальность подтверждается интересом к данному исследованию таких известных ученых, как Нил Джонс !университет Копенгагена) и Люк Онг (университет Оксфорда), с которыми диссертант встречался лично и выступал на семинарах в их исследовательских группах.

Обоснованность и достоверность полученных результатов подтверждается публикациями по материалам диссертации !5 публикапий), включая 2 статьи в журнале, входятцем в Перечень рецензируемых научных изданий, 2 работы в изданиях, входятцих в международную реферативную базу Бсорцз. Все выносимые на защиту результаты в достаточной мере отражены в опубликованных работах.