Онлайн доклад Степана Кузнецова (МИАН, НИУ ВШЭ)
Во вторник, 21 апреля, в 16.40 состоится очередной семинар международной лаборатории статистической и вычислительной геномики
Дорогие коллеги!
Приглашаем Вас послушать онлайн доклад Степана Кузнецова, кандидата физ.-матем. наук, старшего научного сотрудника Математического института им. В.А. Стеклова РАН и Международной лаборатории интеллектуальных систем и структурного анализа ФКН НИУ ВШЭ "Автоматизированное построение и проверка математических доказательств".
Участие в семинаре будет осуществляться посредством инструментария Zoom.
Сыылка для входа: https://zoom.us/j/917650391?pwd=aS8xUVRWcGplb0FFUVdzOE9Fd0x0dz09
Meeting ID: 917 650 391
Password: 078660
Аннотация доклада:
Верификация доказательств быстро становится полезным элементом в работе математиков различных областей. Возможность формальной проверки доказательств теорем особенна ценна в случаях, когда сложность и объём текста доказательства делает его необозримым для человека. Наиболее известные примеры: теорема о четырёх красках и теорема Фейта - Томпсона о разрешимости любой конечной группы нечётного порядка. Один из инструментов автоматизированного построения и проверки доказательств – система Coq. Ещё одним (возможно, даже более важным) применением Coq является разработка программных продуктов, корректность работы которых доказана формально и которые предназначены для использования в критических ситуациях (например, управление опасными производствами). Пример такого продукта – CompCert, верифицированный оптимизирующий компилятор языка Си. Одной из важных специфических черт Coq является возможность конструктивизации доказательства: извлечения реализации алгоритма в виде программы из формального доказательства его корректности.
Приглашаются все желающие.
Если у Вас возникли вопросы, просим Вас обратиться с ними к менеджеру международной лаборатории Шикоте Светлане Каликстовне, sshikota@hse.ru