Blog Archive 2014 Inductive-Recursive Descriptions Aug 04 2014 Modeling Elimination of Described Types Jan 15 2014 An Unremarkable Type Checker Jan 05 2014