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

meta-2018
08:30 - 10:00: Meta - Meta for Types at Cambridge
Chair(s): Elisa Gonzalez BoixVrije Universiteit Brussel
meta-201808:30 - 09:00
Talk
Paventhan VivekanandanIndiana University Bloomington
File Attached
meta-201809:00 - 09:30
Talk
Jim NewtonEPITA / LRDE https://www.lrde.epita.fr, Didier VernaEPITA / LRDE
DOI
meta-201809:30 - 10:00
Talk
Seyed Hossein HaeriUniversité Catholique de Louvain, Paul Keir