Registration form (Registration is free, but mandatory. Please note that while in-person registration is still possible, we will not be able to provide lunch for participants registered after April 12, end-of-day AoE.)
Time | Title | Speakers | Details | |
---|---|---|---|---|
08:30 - 09:30 | welcome | |||
09:30 - 10:00 | Actema as a front-end for Coq | Benjamin Werner | ||
10:00 - 10:45 | The Concepts and Categorical Theory of Graph Rewriting | Reiko Heckel | ||
10:45 - 11:15 | coffee break | |||
11:15 - 11:45 | An interface for diagrammatic proofs in Coq | Luc Chabassier | ||
12:00 - 12:30 | Yet another diagram editor, generating Coq scripts | Ambroise Lafont | ||
12:30 - 14:00 | lunch break | (buffet at meeting venue) | ||
14:00 - 14:45 | A preliminary formalisation of Category Theory using Hierarchy Builder | Cyril Cohen | ||
15:00 - 15:30 | Writing hybrid mathematical documents with coq-lsp | Emilio Jesús Gallego Arias | ||
15:30 - 16:00 | AlgebraicRewriting.jl |
Kristofer Brown | ||
16:00 - 16:30 | coffee break | |||
16:30 - 18:30 | working groups | |||
19:00 | dinner (details TBD) |
Actema
as a front-end for Coq — Benjamin Werner, LIX laboratory, École PolytechniqueActema
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.
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.
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.
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.
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.
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, BerkeleyAn 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.