Приглашённые докладчики

• Илья Сергей — лектор в Университетском колледже Лондона, PhD. Тема доклада: «Зависимые типы для верификации реалистичного кода».

Системы зависимых типов (dependent types) — мощный инструмент для написания корректных программ и формального доказательства математических утверждений. Традиционно, большинство прикладных программистов, знакомых с зависимыми типами, воспринимают их не иначе как элегантную теоретическую концепцию, плохо применимую для чего-то более практичного, чем верификация простых арифметических процедур или операций над списками, написанных чисто функциональном языке.

В этом докладе я расскажу, как использовать зависимые типы для спецификации и верификации “императивного” кода. Мы увидим, как семантика многих аспектов, свойственных “реалистичным” языкам программирования, таких как адресная арифметика, многопоточность и распределенные вычисления, может быть описана при помощи зависимых типов, а корректность использующих их программ—доказана с использованием формальной логики в механизированной среде.

• Екатерина Комендантская — доцент информатики в Школе математики и информатики Университета Хериота-Уатта. Тема доклада: «Сертифицированное автоматизированное доказательство теорем в системах типов».

Существует два основных стиля формальной верификации: (*) алгоритмический, при котором задача верификации формулируется средствами инструментов автоматического доказательства теорем (первого порядка), такими как логическое программирование (с ограничениями) или SMT-решатели, после чего представляющие интерес свойства проверяются автоматически. Соответствующие инструменты могут работать быстро, однако удостовериться в корректности полученных результатов без построения и проверки доказательств довольно трудно. Причина лежит в высокой сложности существующих на данный момент реализаций, так, к примеру, размер кодовой базы SMT-решателей может составлять сотни тысяч строк кода на C++. Эти инструменты содержат ошибки, а значит не могут считаться достаточно корректными для критически важных систем.

Альтернативой является (**) подход, основанный на типах: разработчик может зафиксировать все интересующие его свойства в виде типов функций в своей программе. Благодаря соответствию Карри—Ховарда населяющие соответствующий тип элементы играют роли исполняемых функций и свидетелей корректности, что и завершает цикл сертификации.

В наилучшем случае типы позволяют описать большую часть свойств, представляющих интерес для сообщества верификаторов, к примеру современные диалекты Liquid Haskell и F* позволяют формулировать пред- и постусловия на уровне типов. Но затем выраженные на уровне типов свойства становятся настолько сложными, что системам вывода типов приходится пользоваться инструментами автоматического доказательства: и Liquid Haskell, и F* используют SMT-решатели напрямую. Таким образом, мы снова доверяем вопрос корректности недостаточно сертифицированным инструментам автоматического доказательства.

В этом докладе я расскажу о нашей недавней работе, которая разрешает представленную выше дихотомию «масштаб или корректность», предлагая новый, основанный на типах подход к автоматическому доказательству для систем вывода типов. Мы разработали новый метод использования логического программирования в выводе типов в Haskell: Хорновские дизъюнкты можно представить в виде типов, а доказательства методом резолюции — как населяющие типы термы. В результате автоматические доказательства непосредственно попадают в систему типов и компилятор Haskell, сохраняя при этом высокие стандарты сертификации используемых при выводе типов доказательств.

Доклад основывается на совместной с Пенгом Фу и Томом Шриверсом работе, представленной на конференции FLOPS ’2016.