.GReTA-ExACT

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.
Friday, March 18, 2022 15:00 Europe/Paris
Follow
Hierarchy Builder
Libraries of machine checked code are, nowadays, organized around hierarchies of algebraic structures. Unfortunately the language of Type Theory and the features provided by the Coq system make the construction of a hierarchy hard even for expert users. The difficulty begins with the non-orthogonal choices, between storing information as record fields or parameters, and between using type classes and canonical structures for inference. To this, one may add the concerns about performance and …
Friday, November 26, 2021 15:00 Europe/Paris
Follow
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 …

Friday, November 12, 2021 10:00 Europe/Paris
Follow
GReTA-ExACT: towards Executable Applied Category Theory

This talk marks the beginning of GReTA-ExACT, a new online working group within the GReTA community. The aim of this working group will consist in providing an interdisciplinary forum for exploring the diverse aspects of applied category theory relevant in graph transformation systems and their generalizations, in developing a methodology for formalizing diagrammatic proofs as relevant in rewriting theories via proof assistants such as Coq, and in establishing a community-driven wiki system and …
Friday, November 5, 2021 15:00 Europe/Paris
Follow