The logical relations (Figure 3) in this manuscript are not actually well-defined. Specifically, the definition of R_S(bits)\varphi refers to the definition of R_S(\tau)\varphi for *all* \tau. It is not well-founded, of course! This problem is corrected in the CSFW/JCS version of our paper in an obvious way of adding \tau in bits as bits[\tau], but it makes the calculus far less expressive - strongly normalizing, indeed. ---------- Conjecture 15 (Full Abstraction) at the end of Section 4 (page 17) is solved negatively by Dominique Devriese, Marco Patrignani, and Frank Piessens in their POPL 2018 paper "Parametricity versus the Universal Type".