See:

This version extends the ICFP 17 system with eta-equivalence rules. The pure icfp17 system is available at tag icfp17.

• src for Coq development.

• spec for Ott specification.

• doc for ICFP 17 paper "A Specification for Dependent Types in Haskell".

• doc for CoqPL abstract "Locally Nameless at Scale"

• See paper TYPES 2019 paper "Eta-Equivalence in Core Dependent Haskell" for a description of the modifications needed for eta-equivalence rules.

Acknowledgements This material is based upon work supported by the National Science Foundation under Grant No. 1319880 and Grant No. 1521539.