walker (Feb 01 2023 at 14:16): walker (Feb 01 2023 at 14:16):I am refering to this:
https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/
It feels to me that what they are doing is building model for the language and prove thing based on that model, but then how would that work for things like MLTT/cubicalTT. I assume that would require having a model for cubical sets, BCCC in coq, and I heard horror stories about modelling categories in coq
Does anyone have idea on the usability of such techniques for proving safety of languages like MLTT/CoC ..etc .
Paolo Giarrusso (Feb 01 2023 at 16:09):This has been done for NuPRL, and that’s been formalized in Coq
Paolo Giarrusso (Feb 01 2023 at 16:10):Also, almost all normalization proofs you’ve run into use a variant of semantic typing (historically, the opposite might be true).
Paolo Giarrusso (Feb 01 2023 at 16:14):I also don’t think you need categories necessarily (but I’m hesitant to give recommendations): typically you need categories to describe a (large) class of models, but if you just need a model you can specialize the idea to a suitable category (often, the category of sets in the ambient theory).
walker (Feb 01 2023 at 16:17):I would take the disuccsion to the other thread in iris :sweat_smile: to avoid duplication
Notification Bot (Feb 01 2023 at 16:17):walker has marked this topic as resolved.
Last updated: Jun 05 2023 at 10:01 UTC