Preprint
From Reversible Programs to Univalent Universes and Back
Abstract
We establish a close connection between a reversible programming language
based on type isomorphisms and a formally presented univalent universe. The
Authors
Carette J; Chen C-H; Choudhury V; Sabry A
Publication date
August 9, 2017
DOI
10.48550/arxiv.1708.02710
Preprint server
arXiv