Canonicity and Computability in Homotopy Type Theory
Dmitry Filippov
TL;DR
This paper explores the computational aspects of Martin Lof's dependent type theory, examining whether it can be fully canonical and computable in its semantic representation.
Contribution
It provides an analysis of the canonicity and computability issues within homotopy type theory, highlighting challenges and potential solutions.
Findings
Identifies limitations in current semantic models
Proposes approaches for canonical and computable semantics
Analyzes the implications for homotopy type theory
Abstract
This dissertation gives an overview of Martin Lof's dependant type theory, focusing on its computational content and addressing a question of possibility of fully canonical and computable semantic presentation.
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.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Advanced Topology and Set Theory · Logic, programming, and type systems