Informatics Report Series
|
|
|
|
|
|
Title:A constructive algebraic hierarchy in Coq |
Authors:
Herman Geuvers
; Robert Pollack
; Freek Wiedijk
; Jan Zwanenburg
|
Date:Oct 2002 |
Publication Title:Journal of Symbolic Computation |
Publisher:Elsevier |
Publication Type:Journal Article
Publication Status:Published
|
Volume No:34(4)
Page Nos:271-286
|
DOI:10.1006/jsco.2002.0552
|
- Abstract:
-
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.
- Links To Paper
- No links available
- Bibtex format
- @Article{EDI-INF-RR-0747,
- author = {
Herman Geuvers
and Robert Pollack
and Freek Wiedijk
and Jan Zwanenburg
},
- title = {A constructive algebraic hierarchy in Coq},
- journal = {Journal of Symbolic Computation},
- publisher = {Elsevier},
- year = 2002,
- month = {Oct},
- volume = {34(4)},
- pages = {271-286},
- doi = {10.1006/jsco.2002.0552},
- }
|