Verified algorithmic category theory
Master Project

Project Description

This project aims at bridging the gap between two disciplines of constructive mathematics. The first discipline is that of machine-verified constructive proofs; the second discipline is computer algebra. The first discipline is implicitly algorithmic while the second is so explicitly : The Curry-Howard correspondence, summarized in the slogan “proofs as programs”, states that one can extract programs from constructive proofs. Such program extractions are explicitly possible in the proof assistants Rocq1 , Agda, and LEAN. The quality of such programs can be measured by various metrics, including the complexity of the underlying algorithm it implements. Since correctness is the main focus of practitioners in the proof verification community, the quality of such programs is rarely a real concern. In contrast, the computer algebra community lends ultimate focus on the quality of such programs that often goes beyond complexity consideration and involves other metrics like modularity, maintainability and ultimate efficiency of the implementation. Even though computer algebra relies on the correctness of the algorithms and their implementations, the existing computer algebra systems typically lack the necessary infrastructure for proving ultimate correctness. Summing up, the first community extracts correct but typically inefficient algorithms while the second community implements highly efficient algorithms which are typically without machine-certified correctness proofs.

Computer algebra systems and computer proof assistants have been developed as different tools, by entirely different communities. Cooperation between these tools is currently organized on an ad-hoc basis, often using computer algebra systems as external oracles for computer proof assistants. Bugs in computer algebra systems are thus difficult to uncover. In this project, we aim to develop a framework for a computer algebra system and a computer proof assistant to collaborate in the specific mathematical area of category theory. In this way, we aim to develop algorithmic category theory that is both performant and proven correct.

We firstly build the tightly integrated system VALCT for “Verified ALgorithmic Category Theory”. Secondly, we leverage VALCT to develop a significant library for verified category theory. Specifically, VALCT offers a language for writing categorical algorithms with placeholders for proof obligations. Our library can then be considered as a unified code base that we translate, on the one hand, to a proof assistant, where the proof obligations can be filled, and, on the other hand, to a computer algebra software supporting category theory for performant execution. We implement such translations to Rocq and CAP, respectively. In this way, we leverage two existing systems and their strengths, maintaining a separation of concerns between correctness and performance.

Links:

• https://github.com/homalg-project/CAP_project
• https://rocq-prover.org/

Project Goals

In this project, you will work on the following goals:

• Learn to use the computer algebra system CAP
• Learn to use the computer proof assistant Rocq
• Design a language for category-theoretic algorithms
• Translate this language into Rocq and CAP

Contacts for the Project

• Benedikt Ahrens (TU Delft)