But this is a type system ! I have never heard of adequacy about a type system...

Adequacy of the model of the type system. Soundness would be "syntactic -> semantic", wouldn't it?

I don't know what you mean by "syntactic -> semantic", but to me, the theorem proved here is really type soundness. That is, if the program is well-typed, then the program does not go wrong.

The only thing which is perhaps slightly different than standard type soundness is the fact that we are using a shallow embedding. Is that what you are referring to?

Essentially, yes. I mean "syntactic well-typedness implies semantic well-typedness", i.e. adequacy of the semantic model of the type system. Of course, in a shallow embedding, that's essentially soundness... The other reason is that this theorem looks exactly like what we call adequacy everywhere else in Iris.

I did a quick search on Google, and it seems that what logicians are referring to when speaking about adequacy is soundness AND completeness of a LOGIC (e.g., in first order logic, a formulla is provable if and only if it is true in all models). It seems like there is no such thing as adequacy for a model.

To be frank, I never liked very much the term "adequacy" that we are using for Iris. Do you know where it comes from? I think that, at least, the term "adequacy" does not unambiguously tells what this is about, in contrary to "soundness".

But anyway, for a /type system/, I have never seen the term "adequacy" before, and I can say that "soundness" is the word which is canonically used for that purpose

I concede. I agree we should talk of "type soundness" in the paper, and then calling it "adequacy" in Coq would be weird.

Ok, perfect. Change reverted.