Logical Relations as Types: Proof-Relevant Parametricity for Program Modules — Jonathan Sterling & Robert Harper (2020; J. ACM 68(6) (2021)). arXiv:2010.08599 (v3, PDF).
Proves a proof-relevant, phase-sensitive generalisation of Reynolds’ abstraction theorem for a calculus of ML-style program modules. Logical relations become types in a parametricity type theory, modelled in a topos built by Artin gluing; representation independence is obtained by programming a simulation as a third implementation that carries the representation invariant.
Sources: the paper, arXiv:2010.08599v3, checked against the arXiv listing. Index: Papers.
Key definitions and results
- Theorem 4.1: representation independence for two queue implementations
- Definitions 5.1–5.16: logoi, toposes, open and closed subtopoi
- Theorem 5.18: Artin gluing / recollement
- Construction 5.27: the topos of parametricity structures
- Theorem 5.31, Corollary 5.32: a model of ParamTT; generalised abstraction theorem