Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)
- 17 September 2018
- journal article
- conference paper
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 53 (7), 132-144
- https://doi.org/10.1145/3299711.3242756
Abstract
No abstract availableKeywords
This publication has 13 references indexed in Scilit:
- Refinement reflection: complete verification with SMTProceedings of the ACM on Programming Languages, 2017
- A tale of two provers: verifying monoidal string matching in liquid Haskell and CoqPublished by Association for Computing Machinery (ACM) ,2017
- Dependent types and multi-monadic effects in F*Published by Association for Computing Machinery (ACM) ,2016
- Reasoning with the HERMIT: tool support for equational reasoning on GHC core programsPublished by Association for Computing Machinery (ACM) ,2015
- Refinement types for HaskellPublished by Association for Computing Machinery (ACM) ,2014
- Verified CalculationsLecture Notes in Computer Science, 2014
- Idris, a general-purpose dependently typed programming language: Design and implementationJournal of Functional Programming, 2013
- HALOPublished by Association for Computing Machinery (ACM) ,2013
- Zeno: An Automated Prover for Properties of Recursive Data StructuresLecture Notes in Computer Science, 2012
- Refinement types for MLPublished by Association for Computing Machinery (ACM) ,1991