From Reversible Programs to Univalent Universes and Back
Programming Languages
2019-07-16 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1708.02710,
title = {From Reversible Programs to Univalent Universes and Back},
author = {Jacques Carette and Chao-Hong Chen and Vikraman Choudhury and Amr Sabry},
journal= {arXiv preprint arXiv:1708.02710},
year = {2019}
}