# * Dependent Intersection: A New Way of Defining Records in Type Theory *

## by Alexei Kopylov

2003

Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science.

**Abstract**

Records and dependent records are a powerful tool for programming, representing mathematical concepts, and program verification. In the last decade several type systems with records as primitive types were proposed. The question is arisen: whether it is possible to define record type in existent type theories using standard types without introducing new primitives.

It was known that *independent* records can be defined in type theories with dependent functions or intersection. On the other hand *dependent* records cannot be formed using standard types. Hickey introduced a complex notion of *very dependent functions* to represent dependent records. In the current paper we introduce a simpler type constructor *dependent intersection*, i.e., the intersection of *two* types, where the second type may depend on elements of the first one (do not confuse it with the intersection of a family of types). This new type constructor allows us to define dependent records in a very simple way and also inherently interesting on its own.

**bibTex ref: Kop03**

cite link