|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/5849
| Title: | Quotient Types --- a Modular Approach |
| Authors: | Nogin, Aleksey |
| Keywords: | computer science
technical report |
| Issue Date: | 9-Apr-2002 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2002-1869 |
| Abstract: | In 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. |
| URI: | http://hdl.handle.net/1813/5849 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
