A categorical diagram editor to help formalising commutation proofs
I will present a categorical diagram editor (https://amblafont.github.io/graph-editor/index.html) implemented in Elm that generates Coq proof scripts (based on the UniMath library), letting the user prove manually commutation of each subdiagram. Conversely, the editor can parse a Coq goal stating equality between two composition of morphisms and generate a diagram out of it.
SMTCoq: the power of SMT solving in Coq

SMTCoq is a tool to make the Coq proof assistant and SMT solvers cooperate, with the same degree of confidence as Coq. In this talk, I will give an overview of its potential:

  • checking SMT answers, both in Coq and externally using the Coq extraction mechanism
  • importing SMT problems as Coq theorems
  • calling SMT solvers to ease Coq proof building, in a ongoing project called Sniper.

An API to build first-order SMTCoq terms and formulas is also under progress, in order to have an easy access to …