CoREACT general meeting 2024

Meeting location details

• The meeting will take place in the LIP laboratory, located on the 3rd floor of the main building of the ENS Lyon computer science building. You can access the building on both sides of the walkway between Halle Tony Garnier and the fountain.

• The nearest Metro stop is Debourg; the nearest tram stop is ENS Lyon.

Program

March 11, 2024: Theory Workgroup (Room 394/Salle du Conseil)

March 12, 2024 (morning): Coq/HB workgroup (Room 394/Salle du Conseil)

March 12, 2024 (afternoon): General Meeting (Room M7.315/salle de réunion)

March 13, 2024: Tools/UI-Design Workgroup (Room M7.315/salle de réunion)

Abstracts

Formalizing strict double categories in Coq with HB — Paolo Torrini, Inria Sophia Antipolis

We present different definitions of strict double category in Coq (one based on internal categories, another one on an ad-hoc characterization of pullbacks) and our ongoing work to prove their equivalence.

Progress report on YADE - Yet another diagram editor — Ambroise Lafont, LIX, École Polytechnique

I will present a small but useful UI improvement that allows the user to construct a diagrammatic proof in the editor without having to switch back to the vscode window.

Formalisation of adhesive categories using HB — Samuel Arsac, ENS Lyon

I will present the current state of my formalisation of the hierarchy of categories for rm-quasi-adhesive to adhesive in Coq.

• GitLab project repo: https://gitlab.com/SamuelArsac/graph-rewriting
  
  

Automatic Inference with Elpi : Sets and Structures — Quentin Vermande, Centre Inria d’Université Côte d’Azur

In order to write proofs efficiently, we rely on algorithms that automatically infer informations. For example, we can leave some arguments of a function implicit and even explicitly leave holes in a term, that the system then elaborate on its own. I will show how to improve the inference of structures through a formalization of sets and some basic structures. In particular, I will define a structure of subsets so that membership of a subset can be inferred automatically and then a structure of type equipped with an addition which can be lifted to its subsets. This is achieved using Coq-elpi, a plugin for Coq that provides among other things new and easily extensible algorithms for coercions and typeclasses search.

A nice Quiver + Django + Neo4j + BSS dev workflow for CD database sites — Daniel Donnelly, Jr., Hawaii, USA

Here we explore what can be done if we use said tools in conjunction for the purpose of creating any sort of commutative diagram website.

Certifying Deep Inference steps in Coq — Benjamin Werner, INRIA & LIX, École Polytechnique

The actema interface allows to perform in one action, proof construction steps which can be quite complex in the underlying type theory. In order to allow Coq, working as a back-end for Actema, to perform these steps, I have designed a set of tactics which combine computational reflection and Ltac tactics. I will try to explain some of the difficulties and some chosen solutions.

User interfaces for collaborative diagrammatic proofs: a preliminary roadmap — Emilio Jesús Gallego Arias, IRIF

The CoREACT project aims to build a formalized corpus of category theory definitions and proofs in a collaborative way. A particular emphasis of the project is to enable diagrammatic reasoning and proofs using integrative theorem provers based on type theory, such as Coq or Lean.

A usable realization of this project is a multi-disciplinary, complex project, which involves work on several areas such as document models, incremental computing, metadata, display systems, editors, web technologies…

In this talk, I’d like to present and discuss together a preliminary roadmap towards that goal, based on our experience in developing several users interfaces for the Coq Interative Proof Assistant.