From Reversible Programs to Univalent Universes and Back

conference
Authors
Affiliations

Jacques Carette

McMaster University, Canada

Chao-Hong Chen

Indiana University, USA

Vikraman Choudhury

Indiana University, USA

Amr Sabry

Indiana University, USA

Published

April 16, 2018

Doi

10.1016/j.entcs.2018.03.013

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.

Back to top

Citation

BibTeX citation:
@inproceedings{carette2018,
  author = {Carette, Jacques and Chen, Chao-Hong and Choudhury, Vikraman
    and Sabry, Amr},
  title = {From {Reversible} {Programs} to {Univalent} {Universes} and
    {Back}},
  booktitle = {Electronic Notes in Theoretical Computer Science},
  date = {2018},
  url = {https://doi.org/10.1016/j.entcs.2018.03.013},
  doi = {10.1016/j.entcs.2018.03.013},
  langid = {en},
  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.}
}
For attribution, please cite this work as:
Carette, Jacques, Chao-Hong Chen, Vikraman Choudhury, and Amr Sabry. 2018. “From Reversible Programs to Univalent Universes and Back.” Electronic Notes in Theoretical Computer Science, accepted. https://doi.org/10.1016/j.entcs.2018.03.013.