Mon 5 Nov 2018 08:30 - 09:00 at Cambridge - Meta for Types Chair(s): Elisa Gonzalez Boix

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.

Draft (CodeGenHInd.pdf)673KiB

Mon 5 Nov
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

08:30 - 10:00: Meta for TypesMETA at Cambridge
Chair(s): Elisa Gonzalez BoixVrije Universiteit Brussel
08:30 - 09:00
Code Generation for Higher Inductive Types
Paventhan VivekanandanIndiana University Bloomington
File Attached
09:00 - 09:30
Recognizing heterogeneous sequences by rational type expression
Jim NewtonEPITA / LRDE, Didier VernaEPITA / LRDE
09:30 - 10:00
Multiple Dispatch using Compile-Time Metaprogramming
Seyed Hossein HaeriUniversité Catholique de Louvain, Paul Keir