This repository is a work in progress coq implementation of the equivalence checking of simply typed lambda calculus via logical relations. This is discussed is discussed on the book Advanced Topics in Types and Programming Languages (chapter 6).
We decide to implement our lambda calculus by using the locally nameless representation, which description can be found here
This project depends on:
- mathcomp
You can install mathcomp via opan with the following command
opam install coq-mathcomp-ssreflect