Journal article
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 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 …
Authors
Carette J; Chen C-H; Choudhury V; Sabry A
Journal
Electronic Notes in Theoretical Computer Science, Vol. 336, , pp. 5–25
Publisher
Elsevier
Publication Date
April 2018
DOI
10.1016/j.entcs.2018.03.013
ISSN
1571-0661