This talk presents a co-inductive perspective of provability wherein proofs are no longer finite trees but can be finite graphs, or more generally, non-wellfounded trees. This approach provides a versatile grounding for the mathematical study of recursive and co-recursive concepts, particularly in connection with algorithms, databases and programs. I survey some of the advantages offered by this notion of proof in the form of streamlined soundness and completeness arguments for modal and temporal logics and their applications to interpolation and proof search. Co-inductive proofs have been studied since the early 2000s. Although their appearance was prefigured some thirty years earlier in the form of Schütte’s deduction chains and Mints’ continuous cut elimination, the current interest stems mostly from the seminal work of Niwiński and Walukiewicz on tableaux systems for the modal µ-calculus, and Coquand’s guarded recursion.
Coneris is a novel higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. Coneris builds on the Iris concurrent program logic framework. In the talk I will recall some of the essential logical features of Iris and give an introduction to Coneris.