Cyclic Implicit Complexity

Research output: Working paper/PreprintPreprint

9 Downloads (Pure)


Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common 'recursion schemes'. This paper attempts to bridge the gap between circular proofs and implicit computational complexity. Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify suitable proof theoretical constraints to characterise the polynomial-time and elementary computable functions.
Original languageEnglish
Number of pages53
Publication statusPublished - 3 Oct 2021

Bibliographical note

53 pages, 3 figures


  • cs.LO
  • math.LO


Dive into the research topics of 'Cyclic Implicit Complexity'. Together they form a unique fingerprint.

Cite this