Show simple item record

dc.contributor.authorNogin, Alekseyen_US
dc.description.abstractIn this paper we introduce a new approach to defining quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially chosen set of primitive operations. This modular formalization of quotient types turns out to be very powerful and free of many limitations of the traditional monolithic formalization. To illustrate the advantages of the new formalization, we show how the type of collections (that is known to be very hard to formalize using traditional quotient types) can be naturally formalized using the new primitives. We also show how modularity allows us to reuse one of the new primitives to simplify and enhance the rules for the set types.en_US
dc.format.extent311508 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleQuotient Types --- a Modular Approachen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record