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 .

This has been done for NuPRL, and that’s been formalized in Coq

Also, almost all normalization proofs you’ve run into use a variant of semantic typing (historically, the opposite might be true).

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).

I would take the disuccsion to the other thread in iris :sweat_smile: to avoid duplication

walker has marked this topic as resolved.

Last updated: Sep 25 2023 at 12:01 UTC