Proofs with Cycles in Computation
In January 2025 I began a four-year VR starting grant project Proofs with Cycles in Computation at University of Gothenburg, Sweden.
Project information
- Title: Proofs with Cycles in Computation
- Project size: 4400000 SEK
- Project period: four years
- Institution: Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg, Sweden
- Area: Culture and languages Science and Information Technology
Short description
The project spans four years and aims to develop general theoretical frameworks and novel methodologies for studying cyclic proofs from a computational perspective. Its main objective is to break down the current barriers in the recursion-theoretic interpretation of cyclic proofs, where proof techniques are either missing or tailored to specific settings. The programme is strongly interdisciplinary, ranging from mathematical logic to applied computer science, and builds on a series of preliminary investigations conducted by the applicant in the context of fixed point logics and computational complexity.
Abstract
This research project will advance our mathematical understanding of recursion, i.e., the ability of a program to reiterate itself during computation. Recursion allows us to solve computational tasks by breaking them down into simpler but similar sub-tasks, an essential source of computational power in programming languages.
Mastering recursion is the key to solving problems in complexity theory such as the celebrated P vs. NP problem: is every computational task with an efficiently verifiable solution also efficiently solvable? Approaching the answer to this question is not only of great theoretical importance, it would also directly impact many aspects of modern digital society. Indeed, the security of today's banking systems, for example, crucially relies on the algorithmic difficulty of cracking communication protocols with asymmetric encryption.
Despite its central role, recursion has been considered a "magic box", a primitive indivisible principle that cannot be further analyzed. However, these limitations can be circumvented thanks to a recent development and generalization of mathematical proofs called “cyclic proofs”, which can express recursion and self-iteration via circular reasoning.
Based on the applicant's preliminary research results, the proposed project aims to develop a unified framework for investigating recursion through the lenses of cyclic proofs. The proposed research program spans many areas of mathematics and computer science and aims to further strengthen its interdisciplinary nature with applications of cyclic proofs to software development and formal verification.