Dependent Types

David Aspinall, Martin Hofmann

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract / Description of output

In the most general sense, dependent types are type-valued functions. This definition includes, for example, the type operators of Fω such as Pair. When applied to two types S and T, this yields the type Pair S T whose elements are pairs (s, t) of elements s from S and t from T (see TAPL, Chapter 29). However, the terminology “dependent types” is usually used to indicate a particular class of type-valued functions: those functions which send terms to types. In this chapter we study this kind of dependency.
Original languageEnglish
Title of host publicationAdvanced Topics in Types and Programming Languages
EditorsBenjamin C. Pierce
PublisherMIT Press
Number of pages42
ISBN (Electronic)9780262332668
ISBN (Print)9780262162289
Publication statusPublished - Dec 2004

Cite this