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. © Springer-Verlag Berlin Heidelberg 2002.
Cite
CITATION STYLE
Barthe, G., & Coquand, T. (2002). An introduction to dependent type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2395 LNCS, pp. 1–41). Springer Verlag. https://doi.org/10.1007/3-540-45699-6_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
