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