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.
-
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.