search

coq-community / corn

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
http://c-corn.github.io/
GNU General Public License v2.0
111 stars 43 forks source link

Fundamental theorem of algebra :: location? #74

Open OrenGitHub opened 5 years ago

OrenGitHub commented 5 years ago

Hi guys, quick question: I want to reference your work for a slides assignment on Coq extractions, where can I find the formulation of the fundamental theorem of algebra? A simple grep of your repository got me nowhere ... thanks!

spitters commented 5 years ago

The references are here: http://corn.cs.ru.nl/pub.html Luís Cruz-Filipe, Pierre Letouzey A Large-Scale Experiment in Executing Extracted Programs Electr. Notes Theor. Comput. Sci. 151(1): 75-91 (2006) Luis Cruz-Filipe and Bas Spitters Program extraction from large proof developments. in Proceedings of 16th International Conference TPHOLs 2003 (in LNCS proceedings), D. Basin and B. Wolff (eds.), pages 205--220, LNCS 2758, 2003 Springer-Verlag 2003 pdf

spitters commented 5 years ago

Some of the code is e.g. here: https://github.com/coq-community/corn/tree/master/fta