Higher inductive types are inductive types that include nontrivial higher-dimensional structure, represented as identifications that are not reflexivity. While work proceeds on type theories with a computational interpretation of univalence and higher inductive types, it is convenient to encode these structures in more traditional type theories with mature implementations. However, these encodings involve a great deal of error-prone additional syntax. We present a library that uses Agda’s metaprogramming facilities to automate this process, allowing higher inductive types to be specified with minimal additional syntax.
Mon 5 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
08:30 - 10:00
|Code Generation for Higher Inductive Types|
Paventhan Vivekanandan Indiana University BloomingtonFile Attached
|Recognizing heterogeneous sequences by rational type expression|
|Multiple Dispatch using Compile-Time Metaprogramming|