30 November 2021 to 2 December 2021
Le Bois-Marie
Europe/Paris timezone

Towards Executable Applied Category Theory in Coq (Remote)

30 Nov 2021, 10:00
50m
Centre de conférences Marilyn et James Simons (Le Bois-Marie)

Centre de conférences Marilyn et James Simons

Le Bois-Marie

35, route de Chartres 91440 Bures-sur-Yvette

Speaker

Nicolas Behr (CNRS, Université de Paris, IRIF)

Description

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.

Presentation Materials