Bouncing Threads for Circular and Non-Wellfounded Proofs
David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin
Abstract
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.
Topics & Concepts
Mathematical proofComputer scienceFixed pointPoint (geometry)Proof theoryLeast fixed pointProgramming languageFixed-point theoremMathematicsCalculus (dental)Discrete mathematicsAlgebra over a fieldTheoretical computer sciencePure mathematicsSchauder fixed point theoremGeometryMathematical analysisMedicineDentistryPicard–Lindelöf theoremLogic, programming, and type systemsFormal Methods in VerificationLogic, Reasoning, and Knowledge