TL;DR
This paper explores the deep relationship between reversible programming languages based on type isomorphisms and univalent universes, providing a computational interpretation of paths and univalence.
Contribution
It establishes a formal correspondence linking combinators in reversible programming to paths in univalent universes, bridging programming language theory and homotopy type theory.
Findings
Type isomorphisms correspond to paths in univalent universes
Combinator optimizations relate to 2-paths in the universe
Provides a computational interpretation of univalence
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
