Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

JSC

2002

2002

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...

Related Content

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)