An Introduction to Dependent Type Theory Export

@article{citeulike:4846, abstract = { Functional programming languages often feature mechanisms that involve complex computations at the level of types. These mechanisms can be analyzed uniformly in the framework of dependent types, in which types may depend on values. The purpose of this chapter is to give some background for such an analysis. We present here precise theorems, that should hopefully help the reader to understand to which extent statements like "introducing dependent types in a programming language implies that type checking is undecidable", are justified.}, author = {Barthe, Gilles and Coquand, Thierry}, citeulike-article-id = {4846}, citeulike-linkout-0 = {http://www.metapress.com/content/RX9JB35551V30HQ6}, journal = {Lecture Notes in Computer Science}, keywords = {dependent-types, type-theory}, pages = {1--41}, posted-at = {2005-10-19 17:29:01}, priority = {3}, publisher = {Springer-Verlag Heidelberg}, title = {An Introduction to Dependent Type Theory}, url = {http://www.metapress.com/content/RX9JB35551V30HQ6} }

TY - JOUR ID - citeulike:4846 L3 - citeulike-article-id:4846 N2 - Functional programming languages often feature mechanisms that involve complex computations at the level of types. These mechanisms can be analyzed uniformly in the framework of dependent types, in which types may depend on values. The purpose of this chapter is to give some background for such an analysis. We present here precise theorems, that should hopefully help the reader to understand to which extent statements like "introducing dependent types in a programming language implies that type checking is undecidable", are justified. JF - Lecture Notes in Computer Science EP - 41 TI - An Introduction to Dependent Type Theory PB - Springer-Verlag Heidelberg SP - 1 KW - dependent-types KW - type-theory AU - Barthe, Gilles AU - Coquand, Thierry UR - http://www.metapress.com/content/RX9JB35551V30HQ6 ER -