00:00:00 / 00:00:00

Towards Executable Applied Category Theory in Coq

By Nicolas Behr

Appears in collection : Combinatorics and Arithmetic for Physics: special days

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.

Information about the video

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow


  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
  • Get notification updates
    for your favorite subjects
Give feedback