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.
Time | Title | Speaker(s) | |
---|---|---|---|
13:00 - 14:00 | Overview of the current state of the CoREACT theory developments | Nicolas Behr | |
14:00 - 15:00 | A simple combinatorial starting point for specifying diagrammatic reasoning moves | Tom Hirschowitz & Ambroise Lafont | |
15:00 - 15:30 | coffee break | ||
15:30 - 16:30 | Graphical Algebras | François Métayer | |
16:30 - 18:00 | theory working group session | ||
Time | Title | Speaker | |
---|---|---|---|
09:00 - 09:45 | Automatic Inference with Elpi : Sets and Structures | Quentin Vermande | |
09:45 - 10:30 | Formalizing strict double categories in Coq with HB | Paolo Torrini | |
10:30 - 11:00 | coffee break | ||
11:00 - 12:30 | Coq/HB working group session | ||
12:30 - 14:00 | lunch break | Brasserie des Sciences (approx. 2min from the meeting venue) | |
Time | Title | Speaker | |
---|---|---|---|
14:00 - 14:45 | Formalisation of adhesive categories using HB | Samuel Arsac | |
14:45 - 15:30 | Categorical coherence from term rewriting systems | Samuel Mimram | |
15:30 - 16:00 | coffee break | ||
16:00 - 16:45 | Sketching diagrams and theories | Nicolas Behr | |
16:45 - 17:15 | Progress report on YADE - Yet another diagram editor | Ambroise Lafont | |
17:15 - 18:00 | general discussion | ||
19:00 | dinner | (details TBD) | |
Time | Title | Speaker | |
---|---|---|---|
09:00 - 09:20 | A nice Quiver + Django + Neo4j + BSS dev workflow for CD database sites | Daniel Donnelly | |
09:20 - 10:05 | Certifying Deep Inference steps in Coq | Benjamin Werner | |
10:05 - 10:50 | User interfaces for collaborative diagrammatic proofs: a preliminary roadmap | Emilio Jesús Gallego Arias | |
10:50 - 11:20 | coffee break | ||
11:20 - 13:00 | Coq tools/UI-design workgroup session | ||
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.
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.
I will present the current state of my formalisation of the hierarchy of categories for rm-quasi-adhesive to adhesive in Coq.
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.
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.
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.
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.