@article{sterling_harper_2021, title={Logical Relations as Types: Proof-Relevant Parametricity for Program Modules}, volume={68}, ISSN={1557-735X}, url={http://dx.doi.org/10.1145/3474834}, DOI={10.1145/3474834}, number={6}, journal={Journal of the ACM}, publisher={Association for Computing Machinery (ACM)}, author={Sterling, Jonathan and Harper, Robert}, year={2021}, month=oct, pages={1–47} }