Back to my publicationsXin Yu, Aleksey Nogin, Alexei Kopylov, and Jason Hickey.
Formalizing Abstract Algebra in Type Theory with Dependent Records.
In David Basin and Burkhart Wolff, editors, 16th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging
Trends Proceedings, pages 13–27. Universität Freiburg, 2003.
PDF (257 KB),
PostScript (221 KB).
Our goal is to develop a general formalization of abstract algebra suitable for a general reasoning. One of the most common ways to formalize abstract algebra is to make use of a module system to specify an algebra as a theory. However, this approach suffers from the fact that modules are usually not first-class objects in the formal system. In this paper, we develop a new approach based on the use of dependent record types. In our account, all algebraic structures are first-class objects, with the natural subtyping properties due to record extension (for example, a group is a subtype of a monoid). Our formalization cleanly separates the axiomatization of the algebra from its typing properties, corresponding more closely to a textbook presentation.
Last update: Friday, December 05, 2003 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)