Presentation of "Functorial Diagram Operators" at WADT 2020

At WADT 2020, a Workshop on Algebraic Development Techniques 2020, I delivered a talk on Functorial Diagram Operators – a topic for which I and my advisor Florian Rabe have previously submitted an extended abstract. I am looking forward to us submitting the full paper soon and perhaps even presenting it again if there will be a physical counterpart to the workshop that has happened so far only virtually due to COVID-19.

Updates June 2020:

• Our paper – which we retitled as Structure-Preserving Diagram Operators – is now under peer review for appearing in WADT’s post-proceedings.

• The recording, slides, and abstracts below reflect the version at time of having given the initial talk. After having submitted the full paper, we now know a lot better and would have probably presented it differently.

• We submitted and delivered a very related extended abstract and talk with Diagram Operators in a Logical Framework at LFMTP 2020. The core ideas are the same, but presented differently with different examples, namely for usage of diagram operators for non-compositional logic translations.

📽️ Talk Recording

To be precise, this is only a recording of a rehearsal talk I gave a-priori to myself. The actual talk I gave at WADT 2020 was not recorded.

Latest Slides available here

Fun fact: the headset I wear in the video was useless – I forgot to connect it, so the recording just used the notebook’s audio system 😄

📜 Short Abstract & Extended Abstract

Extended abstract available here

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

Theory operators are meta-level operators in logic that map theories to theories. Often these are functorial in that they can be extended to theory morphisms and possibly enjoy further valuable properties such as preserving inclusions. Thus, it is possible to apply them to entire diagrams at once, often in a way that the output diagram mimics any morphisms or modular structure of the input diagram. We investigate the properties of diagram operators and give numerous examples. All our examples are formalized in the MMT meta-logical framework.