Proofs with Cycles in Computation

This research project is centred around the computational aspects of cyclic proofs, a generalisation of the notion of mathematical proof that offers a natural and systematic approach for modelling recursion.

Its main objective is to develop a broad-spectrum of methodologies and techniques for investigating recursion mechanisms and their computational complexity within the setting of cyclic proof theory.

The project is motivated by (and based on) a series of preliminary results achieved during the applicant´s previous research, which will serve as proof-of-concept, and will be developed by benefiting from a series of national and international collaborations with the foremost experts in the area. The programme covers a four-year time span and is organised in two work packages, each one divided into tasks.

The proposed research has a strong interdisciplinary nature, encompassing a number of theoretical and applied topics within the areas of mathematical logic and computer science, such as Proof Theory, Recursion Theory, Type Theory and Computational Complexity.

In the last part of the programme, the research will pivot towards implementation-oriented goals related to Formal Verification and Theorem Proving, aiming at developing quantitative tools for static certification of runtime efficiency of programs.

Given its innovative and ambitious nature, the proposed research will impact not only theoretical areas but also software development and verification in the long term.