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
30m
Talk
Code Generation for Higher Inductive Types
META
Paventhan VivekanandanIndiana University Bloomington
File Attached
09:00
30m
Talk
Recognizing heterogeneous sequences by rational type expression
META
Jim NewtonEPITA / LRDE https://www.lrde.epita.fr, Didier VernaEPITA / LRDE
DOI
09:30
30m
Talk
Multiple Dispatch using Compile-Time Metaprogramming
META
Seyed Hossein HaeriUniversité Catholique de Louvain, Paul Keir