Dependent Intersection: A New Way of Defining Records in Type Theory
Record types are an important tool for programming and dependent record types are proven to be very useful for program specification and verification. Unfortunately all known embedding of the dependent record type in the type theory had some imperfections. In this paper we present a new type constructor, dependent intersection that allows us to define records that combine the most advantages of previously known approaches, while avoiding most of their disadvantages.
computer science; technical report
Previously Published As