Export to
Friday, September 9, 2016 at 10:31am.
PDXFUNC - Functional Discussions
Access Notes
We're on the 11th floor, come on up. Non-members park bikes outside the building. Paid car parking is connected to the building, and a SmartPark is two blocks away near Target. Located on SW 10th and Washington, between Target and Powell's, on the big block of food carts. We're on the Streetcar line, a block from the Red and Blue MAX lines, and a 5-minute walk from the Green, Yellow, Orange lines.
Website
Description
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.