9–11 Mar 2022
Main
Europe/Berlin timezone

Compiling towers of categories to unlock the full potential of constructive category theory (2/2)

9 Mar 2022, 17:10
30m
Main/2-313 - 313 (Main)

Main/2-313 - 313

Main

30
Show room on map

Speaker

Fabian Zickgraf (Universität Siegen)

Description

As can be seen in the preceding talk ("Constructive Category Theory and Tilting equivalences via Strong Exceptional Sequences" by Kamal Saleh), building constructive towers of categories allows us to reach advanced and complex applications while retaining (relative) simplicity of both the mathematical descriptions and the organization of the software. Our software project CAP (Categories, Algorithms, and Programming) is explicitly designed to facilitate the creation and organization of such towers. This approach allows for modular, reusable, high-level algorithms which are easy to comprehend and check. The only drawback is the computational overhead introduced by the categorical abstraction.

In this talk, we will see various examples of sources of such overhead and how we can again make use of our highly structured setting to compile the high-level code into low-level code by using a compiler explicitly designed for CAP. The compilation process is fully automated and systematic, but can also be easily extended by giving hints for possible optimizations to the compiler. Due to this, the compiler produces better results than either a generic compiler or a manual compilation process could.

This process lifts all the performance restrictions introduced by the categorical abstraction and thus unlocks the full potential of constructive category theory.

Presentation materials