Recursive Subtyping for All

This is the Coq formalization of paper "Recursive Subtyping for All".

• The POPL directory contains the artifact for the conference version of the paper, appeared in POPL 2023.
• The JFP directory contains the artifact for the extended journal version of the paper, which is currently under review.

For detailed building instructions, please refer to the README files in the respective directories.