De Nicolas Behr
This talk will present the ”coreact.wiki” initiative, which aims to develop a novel form of wiki engine that will couple a database of human-readable mathematical knowledge with a database containing machine-readable and -executable representations of this knowledge in proof assistants such as Coq. For the concrete example of analytic combinatorics à la Flajolet and Sedgewick, I will provide an overview of the types of statements that can be efficiently formalized in Coq at present and in the near future, and how we plan to provide an interactive web-based interface to the ”coreact.wiki” platform based upon jsCoq to permit computations and formal proofs in a user-friendly fashion. Time permitting, I will also sketch the possibility of extracting prototypical reference algorithms from formalized categorical statements in Coq via the use of SMT solvers.
De Dimitry Gurevich
De James Propp
De Paul-André Melliès
De Alexandros Singh
De Sergey Yurkevich
De Cyril Banderier
De Stéphane Gaubert
De Vincel Hoang Ngoc Minh
De Lionel Pournin
De Yves André
De Vasudevan Srinivas
