Автоматизация доказательств в LiquidHaskell с помощью реляционных типов

Типы являются полезной абстракцией в языках программирования. Ограничения, накладываемые с помощью типов, позволяют программистам запрещать нежелательные поведения программ, тем самым способствуя их корректности. Для более тщательной верификации программ используют внешние инструменты, в том числе автоматизированное доказательство теорем о программах с помощью языков с зависимыми типами. LiquidHaskell является реализацией типов уточнения для языка Haskell. Приближаясь к выразительности зависимых типов, но обладая большим автоматизмом, эта система позволяет верифицировать некоторые свойства программ на Haskell не прибегая к трудоёмким доказательствам на языках с зависимыми типами. Целью этой работы является автоматизация нового класса доказательств в LiquidHaskell за счёт расширения системы типов реляционными правилами типизации. Прошлые исследования реляционных типов показывают, что в число новых автоматически доказываемых утверждений войдёт ряд интересных свойств из области безопасности и защиты данных. В данной работе формализуется алгоритмическая реляционная система типов, описывается её реализация и тестирование для Haskell и приводятся результаты сопоставления системы с предшественниками.