Proofs are programs, this is Curry-Howard correspondence. What about cyclic proofs, which are graphs rather than trees? We will show how cyclic proofs can be seen as recursive programs, and how various restrictions of the chosen logic make it possible to characterise certain complexity classes: regular and logspace languages; primitive recursive functions, and Peano-definable functions. To this end, we will use some tools from reverse mathematics.
Joint work with Denis Kuperberg & Laureline Pinault.