Presentation of "Diagram Operators in a Logical Framework" at LFMTP 2020

At LFMTP 2020 – Logical Frameworks and Meta-Langauges: Theory and Practice, I delivered a talk on Diagram Operators in a Logical Framework – a topic for which I and my advisor Florian Rabe have previously submitted an extended abstract.

The raw contents are closely related to the talk and submitted paper on Functorial Diagram Operators, however presented in a different light for a different audience.

📽️ Talk Recording

(my talk starts at 0:32)

Latest Slides available here

📜 Short & Extended Abstract

Extended abstract available here

For convenience, here is an emphasized copy of the short abstract:

Module systems for logical frameworks allow building logics and calculi component-wise from small self-contained building blocks. While this enables a high degree of reuse, we still observed many situations where a module system was not sufficient to eliminate redundancy. One particular source of redundancy are module-level syntactic transformations that are entirely formulaic and therefore automatable, but also too complex to capture in typical module systems. In order to overcome this, we introduced the concept of diagram operators and implemented it in the MMT framework (which allows implementing various LF-style logical frameworks). In this paper, we show how we apply diagram operators to eliminate redundancy in large modular libraries of logic formalizations. This enables building many related formalizations in a systematically related way, which simplifies the formalization process and enhances its results, while massively reducing the maintenance cost.