Coinduction in Liquid Haskell
This repository contains encodings of coinductive features in Liquid Haskell. Namely:
- Co-inductive proofs, as explained in Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell. The code relevant to the paper is located in branch haskell22 and also in src/Paper.
- Checks for productivity of corecursive functions, which are discussed in my thesis.