complete dynamics, progress and preservation
Closed this issue · 7 comments
write out the dynamics for complete terms and do the proofs that show that we're type safe without holes (should be easy)
i had thought of them mostly as due diligence? like they're true and i don't think especially tricky. do you think it's just noise we don't need?
I mean, you'll need machinery for substitution etc. We don't make any specific claims wrt the dynamics in the paper -- only that you could give complete expressions a standard dynamics.
Maybe if you can find a clean existing STLC formalism in agda that you can map complete terms into, but I wouldn't bother for POPL.
i believe substitution is pretty trivial because of barendrecht's convention, at least. but statements of the form "substitution is easy because of X" are exactly the sort of thing one lives to regret.
yeah... do this last if you want to do it.
yeah, i agree.
per discussion, we've decided to not include this in the artifact because it's so standard.