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