Speaker
Max Demirdilek
(Universität Hamburg)
Description
Connectives like “and” and “or” allow us to construct sentences—whether in natural language, formal logic, or programming. In classical logic, variables within these sentences can be freely copied or discarded. However, when variables represent resources—such as quantum information—that freedom is no longer appropriate. This has motivated linear logic, a resource-sensitive refinement of classical logic.
Linear logic has models in category theory, some of which have recently been shown to arise from two-dimensional quantum field theories. I will show that calculations and proofs in these categorical models can be carried out using a rigorous three-dimensional graphical language, supported by the computer implementation homotopy.io.
Authors
Christoph Schweigert
(Universität Hamburg)
Max Demirdilek
(Universität Hamburg)
