Revisiting Parametricity: Inductives and Uniformity of Propositions
Reynolds’ 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.
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
16:00 - 18:05
Semantics and SynthesisCoqPL at Watercourt A
Chair(s): Ilya Sergey University College London
|Phantom Types for Quantum Programs|
Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of PennsylvaniaFile Attached
|Revisiting Parametricity: Inductives and Uniformity of Propositions|
Abhishek Anand Cornell University, Greg Morrisett Cornell UniversityFile Attached
|Towards Context-Aware Data Refinement|
Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue UniversityFile Attached
|Mechanizing the Construction and Rewriting of Proper Functions in Coq|
Edwin Westbrook Galois, Inc.File Attached
|A calculus for logical refinements in separation logic|
Dan Frumin Radboud University, Robbert Krebbers Delft University of TechnologyFile Attached