loading...
Dependent Intersection: A New Way of Defining Records in Type Theory
Ottawa, Canada June 22-June 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2003.121004818th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Alexei Kopylov, Cornell University
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 arose: 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 extend Martin-L?f?s type theory with 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 (not to be confused with the intersection of a family of types). This new type constructor allows us to define dependent records in a very simple way. It also allows us to define the set type constructor.
Citation:
Alexei Kopylov, "Dependent Intersection: A New Way of Defining Records in Type Theory," lics, pp.86, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.