Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 16:10 - 16:20 at POPL-B - Semantics

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00: SemanticsPOPL at POPL-B
16:00 - 16:10
Talk
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
POPL
Chao-Hong ChenIndiana University, Amr SabryIndiana University
Link to publication DOI
16:10 - 16:20
Talk
Internalizing Representation Independence with Univalence
POPL
Carlo AngiuliCarnegie Mellon University, Evan CavalloCarnegie Mellon University, Anders MörtbergDepartment of Mathematics, Stockholm University, Max ZeunerStockholm University
Link to publication DOI
16:20 - 16:30
Talk
Petr4: Formal Foundations for P4 Data Planes
POPL
Ryan DoengesCornell University, Mina Tahmasbi ArashlooCornell University, Santiago BautistaUniv Rennes, ENS Rennes, Inria, IRISA, Alexander ChangCornell University, Newton NiCornell University, Samwise ParkinsonCornell University, Rudy PetersonCornell University, Alaia Solko-BreslinCornell University, Amanda XuCornell University, Nate FosterCornell University
Link to publication DOI Pre-print
16:30 - 16:40
Talk
The (In)Efficiency of Interaction
POPL
Beniamino AccattoliInria & Ecole Polytechnique, Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Gabriele VanoniUniversity of Bologna & INRIA Sophia Antipolis
Link to publication DOI
16:40 - 16:50
Talk
Functorial Semantics for Partial Theories
POPL
Chad NesterTallinn University of Technology, Ivan Di LibertiCzech Academy of Sciences, Fosco LoregianTallinn University of Technology, Pawel SobocinskiTallinn University of Technology
Link to publication DOI
16:50 - 17:00
Break
Break
POPL