Functional Discussions


Echo Nolan will be presenting the paper "Generic Constructors and Eliminators from Descriptions: Type Theory as a Dependently Typed Internal DSL" by Tim Sheard and Larry Diehl. The authors describe a method of encoding inductive types via descriptions that are ordinary terms, rather than each inductive type adding a new set of axioms to the theory. They go on to contribute a generic eliminator function that works for any type defined in this way.