Dear Gyesik, Thanks for your interest! We are just in the process of updating the contribs so that corn compiles with trunk again. I will check again about the status. However, I believe the current version should compile with 8.4pl4.
Please note that we have made a partial transition to the more modern use of type classes, the math-classes library. http://math-classes.org/ It is a submodule of: https://github.com/c-corn The older parts of the code still work, but you will not get the type class magic. There are many interesting projects. Personally, within constructive analysis, I am very interested in combining proving with computation inside Coq. If you are interested in this direction, as a very initial experiment, one could try to port some more algorithms from Reals/Fast to Reals/Faster. The latter is indeed faster and uses type classes. Another project I thought about was fast numerical computation. Here is a possible development in constructive analysis: http://arxiv.org/abs/1202.3460 Another possible direction is the correctness proof of Newton iteration. I can suggest some more depending on your taste. Best, Bas PS: We have a small meeting planned with Nicolas Magaud, just after TYPES, to connect the corn library with their library for non-standard analysis. PPS: The homepage http://corn.cs.ru.nl/ is not up to date, we should really do something about it. On Tue, Apr 29, 2014 at 5:57 PM, Gyesik Lee <[email protected]> wrote: > Dear C-Corn developers/users, > > I and my students are strongly interested in formalizing constructive > mathematics. > Although we are originally mathematicians and have some experience in > using Coq, dealing with pure mathematics in Coq is new for all of us. So we > are wondering whether the C-Corn project is a good starting point for us, > which we hope strongly. > > Currently we are in the phase of thinking of and looking for some well > known and interesting, but hopefully not so difficult mathematical theorems > which we could set as our first target. > > We also looked at Freek Wiedijk's "Formalizing 100 Theorems" website, but > we are not sure which parts of the C-Corn library provide a good base for > some of the theorems mentioned there. > > We haven't yet checked all the contents of the C-Corn library. So we will > be highly grateful when you can give some hints about or information of the > current state of the library. > > Thanks in advance > > Gyesik > _______________________________________________ > C-CoRN mailing list > [email protected] > http://mailman.science.ru.nl/mailman/listinfo/c-corn >
_______________________________________________ C-CoRN mailing list [email protected] http://mailman.science.ru.nl/mailman/listinfo/c-corn
