Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
..
Failed to load latest commit information.
Makefile
README.md
SfLib.v
dot.v
dsubsup.v
fsub.v
fsub_equiv.v
fsub_exn.v
fsub_mut.v
fsubsup.v
stlc.v

README.md

Type Soundness Proofs with Definitional Interpreters

Paper (POPL 2017): [pdf]

The Coq scripts compile with the command make, using coqc --version 8.4pl6 (July 2015).

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.