Informatics Report Series


Report   

EDI-INF-RR-0747


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh