CoREACT kick-off meeting 2023

• Meeting location details

Program

Abstracts

Actema as a front-end for Coq — Benjamin Werner, LIX laboratory, École Polytechnique

Actema is an user interface that allows to construct formal proofs through graphical actions. It is an attempt to widen the approach pioneered by the proof-by-pointing effort in the 1990ties and is currently at a prototype stage. From a proof-theoretical point of view, it implements a form of deep inference.
We have interfaced Actema with Coq, so that it becomes the front-end of the proof system. I will present this Coq-Actema combination, and try to focus on some aspects that may be relevant or have some relation with the CorREACT project. In particular how the actions are translated into Coq proof objects, using computational reflection.

The Concepts and Categorical Theory of Graph Rewriting — Reiko Heckel, Department of Computer Science, University of Leicester, UK

Categorical formalisations and proofs have been fundamental to the theory of graph rewriting from the beginning in the early 70ies. Most developments since have been elaborations on the classical double-pushout, which formalises the application of a rule as a sequence of a deletion and gluing represented by two pushouts.

To illustrate the use of category theory in graph rewriting we will introduce basic concepts and their representations by diagrams and outline some key theorems and proofs, such as rules and rule applications in both the graphs-as-objects and the graphs-as-arrows views and the Parallelism Theorem relating independent sequential with parallel rewriting steps.

An interface for diagrammatic proofs in Coq — Luc Chabassier, LSV, CNRS & ENS Paris-Saclay

Commutative diagrams are an intuitive and powerful way to reason about equational systems in category theory. However, their graphical nature means they cannot really be encoded in text based proof assistants, such as Coq. To tackle this, we developped a Coq plugin that can extract such a graph from the context of the proof, and display it in an interface, allowing reasonning directly on the graph. Furthermore, once the interaction is finished a Coq proof term is generated that corresponds to the manipulations done to the graph.

A preliminary formalisation of Category Theory using Hierarchy Builder ; Cyril Cohen and/or Enrico Tassi — Cyril Cohen, Inria Sophia-Antipolis Méditerranée, Sophia-Antipolis

In conventional mathematical practices, category theory relies heavily on sharing notation and concepts. However when formalized, Coq’s foundation lacks inherent flexibility to achieve that. Even with the current elaboration mechanisms, such as typeclasses or canonical structures, it becomes verbose due to the challenges in designing the right meta-programs for maintaining consistent notation for various morphisms. To tackle this problem, we provide the domain-specific language Hierarchy Builder (HB) for declaring interfaces and mathematical structures, which programs Coq’s elaborator behind the scenes to enable overload management. By employing this approach, we successfully program the start of a hierarchy of categories, demonstrating the potential of HB and its benefits in implementing program elaboration for Coq. We recommend transferring results from other category libraries using the same methodology, so as to form a solid foundation for the CoREACT project.

Yet another diagram editor, generating Coq scripts — Ambroise Lafont, Department of Computer Science and Technology, University of Cambridge

I will present my diagram editor I use to draw categorical diagrams and generate skeleton Coq proof scripts based on the UniMath library on category theory. It is implemented in the Elm programming language and runs in a web browser. It can also be run as a standalone application (based electron) that can be used in combination with a LaTeX editor (LyX or plain TeX). I will demonstrate various editing features and discuss future work.

Writing hybrid mathematical documents with coq-lsp — Emilio Jesús Gallego Arias, Université de Paris, Inria, CNRS, IRIF

coq-lsp is a new user interface for the Coq proof assistant; based on the experience with previous projects such as jsCoq or SerAPI, coq-lsp aims to provide a natural workflow to mathematicians and computer scientists willing to write down papers that mix both mechanized and natural-language mathematics.

We will present coq-lsp capabilities and demonstrate its workflow in two scenarios: as a Visual Studio Code plugin, and as a standalone tool using jsCoq and the Curvenote scientific editor.

AlgebraicRewriting.jl — Kristofer Brown, Topos Institute, Berkeley

An overview of the current and planned features of AlgebraicRewriting.jl, a graph rewriting package designed to be expressive, extensible, and fast. Current features include working in many categories (e.g. C-Sets, slices thereof, diagrams thereof), using semantics like SPO/SqPO/PBPO+, a DSL for application conditions (e.g. negative application conditions, lifting conditions), handling of both combinatorial and attribute data, concurrency analysis via graph processes, and a graphical language for general purpose programming via graph rewriting.