In mainstream mathematics, non-finite notions of proofs are not considered as formal arguments in their own right, but merely as an intermediate machinery in formal investigations. Over time, however, they have proven to be an important alternative to finitary proofs and, in the last decade in particular, have helped break important barriers in our utilisation of recursion and co-recursion. These principles are ubiquitous in mathematics and computer science, lying at the core of mathematical proofs, computer algorithms and data structures. This project is about cyclic proofs, a subclass of non-finite proofs which, albeit infinitary, can be represented as finite graphs. The overarching goal is to provide a uniform theory for cyclic proof systems and I will approach the problem by investigating two computationally relevant extensions of modal logic: 1. Intuitionistic cycles. Design a robust logical framework for intuitionistic modal logic with fixed points, and develop general methods to establish fundamental properties such as decidability and algorithmic proof search. 2. Higher-type cycles. Establish a strong and succinct mathematical theory for model checking computation trees of higher-type functional programs. To carry out the investigation I will combine traditional methods from formal language theory (game and automata characterisations) with abstract formalisations provided by mathematical logic (sequent calculi, tableaux representa- tions, cyclic proof theory).