From Reversible Programs to Univalent Universes and Back

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.


Publication Date:
Apr 16 2018
Date Submitted:
Jun 28 2019
Pagination:
43610
Citation:
Electronic Notes in Theoretical Computer Science
336
External Resources:




 Record created 2019-06-28, last modified 2019-07-11


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)