Mechanizing type environments in weak HOAS

We take as case study the type language of Sistem F_<: and achieve in Coq the following results:

• contribution 1 [script]
• proof of the POPLmark Challenge 1A, by using a deep encoding of subtyping;
• internal equivalence (adequacy) between the deep encoding and a shallow one.
• contribution 2 [script]
• proof of the POPLmark Challenge 1B, by using an extension of the deep encoding.

Our research has been published by Theoretical Computer Science.