unofficial copies [PDF], [PS]

by Alexei Kopylov

Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science, pp. 86-95, 2003.

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.