Laboratoire d'informatique de l'École polytechnique

A diagram editor to mechanise categorical proofs

Speaker: Ambroise Lafont
Location: Amphi Gilles Kahn + webex
Date:

Diagrammatic proofs are ubiquitous in certain areas of mathematics, especially in category theory. Mechanising such proofs is a tedious task because proof assistants (such as Coq) are text based. We present a prototypical diagram editor to make this process easier, building upon the vscode extension coq-lsp for the Coq proof assistant and a web application (you can try it on my personal website).