Sciweavers

Share
JSC
2002

A Constructive Algebraic Hierarchy in Coq

8 years 11 months ago
A Constructive Algebraic Hierarchy in Coq
We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof of the Fundamental Theorem of Algebra has been formalized in Coq. braic hierarchy that is described here is both abstract and ed. Structures like groups and rings are part of it in an abstract way, defining e.g. a ring as a tuple consisting of a group, a binary operation and a constant that together satisfy the properties of a ring. In this way, a ring automatically inherits the group properties of the additive subgroup. The algebraic hierarchy is formalized in Coq by applying a combination of labeled record types and coercions. In the labeled record types of Coq, one can use dependent types: the type of one label may depend on another label. This allows to give a type to a dependent-typed tuple like A, f, a , where A is a set, f an operation on A and a an element of A. Coercions are functions that are used i...
Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 2002
Where JSC
Authors Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg
Comments (0)
books