DICoq

Dependent Interoperability for Coq

The repository contains the companion code of the publication Partial Type Equivalences for Verified Dependent Interoperability (ICFP'16).

You can browse the code here starting from the compiler example (or directly the toc)