Papers › Revisiting Parametricity: Inductives and Uniformity of Propositions
Revisiting Parametricity: Inductives and Uniformity of Propositions
Abhishek Anand, Greg Morrisett
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
Reynold's parametricity theory captures the property that parametrically polymorphic functions behave uniformly: they produce related results on related instantiations. In dependently-typed programming languages, such relations and uniformity proofs can be expressed internally, and generated as a program translation. We present a new parametricity translation for a significant fragment of Coq. Previous translations of parametrically polymorphic propositions allowed non-uniformity. For example, on related instantiations, a function may return propositions that are logically inequivalent (e.g. True and False). We show that uniformity of polymorphic propositions is not achievable in general. Nevertheless, our translation produces proofs that the two propositions are logically equivalent and also that any two proofs of those propositions are related. This is achieved at the cost of potentially requiring more assumptions on the instantiations, requiring them to be isomorphic in the worst case. Our translation augments the previous one for Coq by carrying and compositionally building extra proofs about parametricity relations. It is made easier by a new method for translating inductive types and pattern matching. The new method builds upon and generalizes previous such translations for dependently-typed programming languages. Using reification and reflection, we have implemented our translation as Coq programs. We obtain several stronger free theorems applicable to an ongoing compiler-correctness project. Previously, proofs of some of these theorems took several hours to finish.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections