[TYPES] Translation of bounded quantifications into intersection types

[Ningning Xie]

We have been working on an intersection type system.

In the dissertation of Benjamin Pierce
(https://www.cis.upenn.edu/~bcpierce/papers/thesis.pdf), Section 3.5.1 and
7.9
mentioned a rough idea of translating bounded quantifications (System F-sub)
into intersection types.

Wondering if there is any related work/formalization in this direction?

Thanks in advance for pointers!


Best regards,
Ningning