sweirich
released this
20 Nov 14:39
·
52 commits
to main
since this release
This release contains Coq proofs for the type soundness proof described in Section 7.2 of the POPL 2021 paper "A Graded Dependent Type System with a Usage-Aware Semantics"