Bouncing Threads for Circular and Non-Wellfounded Proofs
David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin · 2022
Given that (co)inductive types are naturally modelled as fixed points, it is unsurprising that fixed-point logics are of interest in the study of programming languages, via the Curry-Howard (or proofs-as-programs) correspondence. This motivates investigations of the structural proof-theory of fixed-point logics and of their cut-elimination procedures.