Back to my publicationsAleksey Nogin
Quotient Types: A Modular Approach.
In Victor A. Carreño, Cézar A. Muñoz, and
Sophiène Tahar, editors, Proceedings of the 15th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002),
volume 2410 of Lecture Notes in Computer Science, pages 281--297.
Springer-Verlag, 2002.
LNCS
Entry, PDF (271KB), PS (886 KB)
Earlier version:
Aleksey Nogin
Quotient Types — a Modular Approach.
Department of Computer Science TR2002-1869, Cornell University, April 2002
Cornell Tech Reports
Entry, PDF (304KB), PostScript (245KB)
In this paper we introduce a new approach to axiomatizing 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 much easier to use and free of many limitations of the traditional monolithic formalization. To illustrate the advantages of the new approach, 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.
Last update: Monday, October 20, 2003 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)