Stream: Miscellaneous

Topic: ✔ can Semantic Typing be done in coq?


view this post on Zulip 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 .

view this post on Zulip Paolo Giarrusso (Feb 01 2023 at 16:09):

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

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip walker (Feb 01 2023 at 16:17):

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

view this post on Zulip Notification Bot (Feb 01 2023 at 16:17):

walker has marked this topic as resolved.


Last updated: Jun 05 2023 at 10:01 UTC