Wellfounded Trees and Dependent Polynomial Functors Export

@incollection{citeulike:4234183, abstract = {We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by investigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed categories.}, author = {Gambino, Nicola and Hyland, Martin}, citeulike-article-id = {4234183}, citeulike-linkout-0 = {http://www.springerlink.com/content/j5nelqtdptmt4e5v}, journal = {Types for Proofs and Programs}, keywords = {category-thoery, dependent-types, type-theory}, pages = {210--225}, posted-at = {2009-03-28 13:51:23}, priority = {0}, title = {Wellfounded Trees and Dependent Polynomial Functors}, url = {http://www.springerlink.com/content/j5nelqtdptmt4e5v}, year = {2004} }

TY - CHAP ID - citeulike:4234183 L3 - citeulike-article-id:4234183 N2 - We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by investigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed categories. JF - Types for Proofs and Programs EP - 225 TI - Wellfounded Trees and Dependent Polynomial Functors SP - 210 KW - category-thoery KW - dependent-types KW - type-theory AU - Gambino, Nicola AU - Hyland, Martin PY - 2004/// UR - http://www.springerlink.com/content/j5nelqtdptmt4e5v ER -