From Reversible Programs to Univalent Universes and Back
Carette, Jacques; Chen, Chao-Hong; Choudhury, Vikraman; Sabry, Amr A.
2018

Abstract

We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combinators witnessing type isomorphisms in the programming language to paths in the univalent universe; and combinator optimizations in the programming language to 2-paths in the univalent universe. The result suggests a simple computational interpretation of paths and of univalence in terms of familiar programming constructs whenever the universe in question is computable.

Details

Title From Reversible Programs to Univalent Universes and Back
Author Carette, Jacques
Chen, Chao-Hong
Choudhury, Vikraman
Sabry, Amr A.
Publication Date Apr 16 2018
Date Submitted Jun 28 2019
DOI https://doi.org/10.1016/j.entcs.2018.03.013
Pagination 43610
Published in Electronic Notes in Theoretical Computer Science
Volume 336
External Resources https://doi.org/10.1016/j.entcs.2018.03.013

Statistics

from
to
Export