Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
Journal of the ACM

After going to press, we have fixed the following mistakes:

  1. In the definition of a logos, we mistakenly said that "colimits commute with finite limits" but we meant to say that they commute with pullbacks. We thank Sarah Rovner-Frydman for noticing this mistake.
  2. In Remark 5.15, we used the notation for the closed immersion prior to introducing it.

The local copy linked here has the corrections implemented.