Internalizing representation independence with univalence
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 04, 2021
- Source ID
- 10.1145/3434293
Entities
People
- Anders Mörtberg
- Carlo Angiuli
- Evan Cavallo
- Max Zeuner
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University
- Stockholm University
- Swedish Research Council