Name
Abstract | ||
|---|---|---|
Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the computational behavior of HITs. Computational interpretations have now been provided for univalence and specific HITs by way of cubical type theories, which use a judgmental infrastructure of dimension variables. We extend the cartesian cubical computational type theory introduced by Angiuli et al. with a schema for indexed cubical inductive types (CITs), an adaptation of higher inductive types to the cubical setting. In doing so, we isolate the canonical values of a cubical inductive type and prove a canonicity theorem with respect to these values.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3290314 | Proceedings of the ACM on Programming Languages |
Keywords | Field | DocType |
cubical type theory,higher inductive types,homotopy type theory | Inductive type,Algebra,Computer science,Axiom,Type theory,Theoretical computer science,Homotopy type theory,Schema (psychology),Cartesian coordinate system | Journal |
Volume | Issue | ISSN |
3 | POPL | 2475-1421 |
Citations | PageRank | References |
2 | 0.37 | 15 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Evan Cavallo | 1 | 2 | 2.06 |
| Robert Harper | 2 | 11 | 2.76 |