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"
Acknowledgements This material is based upon work supported by the National Science Foundation under Grant No. 1319880 and Grant No. 1521539.