Liquid Haskell - это программный верификатор для Haskell, который позволяет разработчикам указывать свойства корректности, используя типы уточнения . [1] [2] Свойства проверяются с помощью SMT- решателя, совместимого с SMTLIB2 , например, средства доказательства теорем Z3 .
Смотрите также
Рекомендации
- ^ Vazou, Niki (2016). Liquid Haskell: Haskell как средство доказательства теорем (Диссертация). Калифорнийский университет.
- ^ Вазу, Ники; Зайдель, Эрик (2014). «Типы уточнения для Haskell» . Материалы 19-й Международной конференции ACM SIGPLAN по функциональному программированию . Международная конференция по функциональному программированию. ACM. С. 269–282. DOI : 10.1145 / 2692915.2628161 .
- Лё, Андрес (2018). Мастерская Liquid Haskell . ЛПП 2018.
- Джала, Ранджит (2014). Liquid Haskell . Группа пользователей Boston Haskell.
дальнейшее чтение
- Вазу, Ники. Liquid Haskell: типы уточнения для Haskell . 45-й симпозиум ACM SIGPLAN по принципам языков программирования (POPL 2018).
- Дьячки, Явор (2015). «Улучшение типов Haskell с помощью SMT». Материалы 8-го симпозиума ACM SIGPLAN по Haskell - Haskell 2015 . ACM. С. 1–10. DOI : 10.1145 / 2804302.2804307 . ISBN 9781450338080.
Внешние ссылки
- «Жидкий Haskell - HaskellWiki» . wiki.haskell.org . Проверено 31 марта 2019 года .