Paper (POPL 2017): [pdf]
The Coq scripts compile with the command make, using coqc --version 8.4pl6 (July 2015).
- STLC
- F<:
- F<: Equivalence with Small-Step
- F<: with Mutable References
- F<: with Exceptions
- F<:> from the System D Square
- D<:> from the System D Square
- DOT in Big-Step
For Step-by-Step Instructions, please see Appendix A of the paper (Type Soundness Proofs with Definitional Interpreters), which outlines a correspondence between the formalisms in the paper and in Coq.