Видеотека: П. П. Соколов, Формальная верификация на Arend

ВИДЕОТЕКА


Однодневный семинар по математической логике 29 июня 2023 г. 16:00, г. Москва, Покровский бульвар 11, аудитория R201

Формальная верификация на Arend П. П. Соколов
Аннотация: В докладе будет представлен Arend, инструмент интерактивного доказательства теорем, основанный на гомотопической теории типов. Мы рассмотрим принцип работы и логические основания таких инструментов, отличительные особенности Arend, а также рассмотрим несколько примеров классических задач формальной верификации и их решений на Arend.