Tool Support for Graphical Categorical Reasoning

Supervisors

Suitable for

Abstract

Recent work has demonstrated how a suitable form of string diagrams can provide a powerful tool for reasoning in elementary category theory. Currently these diagrams are laid out and manipulated manually, as good layout choices are important for aiding the intuitions of readers. The project would involve investigating appropriate tool support for working with these diagrams, and ideally to provide a prototype implementation to demonstrate some of the ideas involved. The emphasis will be on convenient layout of practically useful diagrams that convey the correct geometric intuitions, rather than proof automation as provided by the Quantomatic tool for similar graphical calculi.

Prerequisites: A good knowledge of elementary category theory is essential. Some experience with string diagrams, as for example in the quantum computer science courses in the department would be helpful. Good programming skills in at least one language will be needed for prototyping.