Internalizing Representation Independence with Univalence
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky’s univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations.
In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.
Wed 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00
|A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types|
Chao-Hong Chen Indiana University, Amr Sabry Indiana UniversityLink to publication DOI
|Internalizing Representation Independence with Univalence|
Carlo Angiuli Carnegie Mellon University, Evan Cavallo Carnegie Mellon University, Anders Mörtberg Department of Mathematics, Stockholm University, Max Zeuner Stockholm UniversityLink to publication DOI
|Petr4: Formal Foundations for P4 Data Planes|
Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell UniversityLink to publication DOI Pre-print
|The (In)Efficiency of Interaction|
Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna, Italy / Inria, France, Gabriele Vanoni University of Bologna & INRIA Sophia AntipolisLink to publication DOI
|Functorial Semantics for Partial Theories|
Chad Nester Tallinn University of Technology, Ivan Di Liberti Czech Academy of Sciences, Fosco Loregian Tallinn University of Technology, Pawel Sobocinski Tallinn University of TechnologyLink to publication DOI