@inproceedings{10.1145/3531130.3533375,
    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. Among the various approaches to proofs in fixed-point logics, circular -- or cyclic -- proofs, are of interest in this regard but suffer from a number of limitations, most notably from a quite restricted use of cuts. Indeed, the validity condition which ensures soundness of non-wellfounded derivations and productivity of their cut-elimination prevents some computationally-relevant patterns of cuts. As a result, traditional circular proofs cannot serve as a basis for a theory of (co)recursive programming by lack of compositionality: there are not enough circular proofs and they compose badly. The present paper addresses some of these limitations by developing the circular and non-wellfounded proof-theory of multiplicative additive linear logic with fixed points () beyond the scope of the seminal works of Santocanale and Fortier and of Baelde et al. We define bouncing-validity: a new, generalized, validity criterion for , which takes axioms and cuts into account. We show soundness and cut elimination theorems for bouncing-valid non-wellfounded proofs: as a result, even though bouncing-validity proves the same sequents (or judgments) as before, we have many more valid proofs at our disposal. We illustrate the computational relevance of bouncing-validity on a number of examples. Finally, we study the decidability of the criterion in the circular case: we prove that it is undecidable in general but identify a hierarchy of decidable sub-criteria.},
    Address = {New York, NY, USA},
    Author = {Baelde, David and Doumane, Amina and Kuperberg, Denis and Saurin, Alexis},
    BookTitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
    File = {Bouncing Threads for Circular and Non-Wellfounded Proofs - 3531130.3533375.pdf},
    ISBN = {9781450393515},
    Keywords = {Linear Logic., Circular Proofs, Fixed Points, Curry-Howard, Coinduction, Decidability, Cut Elimination},
    Location = {Haifa, Israel},
    Publisher = {Association for Computing Machinery},
    Series = {LICS '22},
    Title = {Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs},
    URL = {https://doi.org/10.1145/3531130.3533375},
    Year = {2022},
    articleno = {63},
    bdsk-url-1 = {https://doi.org/10.1145/3531130.3533375},
    date-added = {2022-08-29 14:27:27 +0200},
    date-modified = {2022-08-29 14:27:27 +0200},
    numpages = {13},
    doi = {10.1145/3531130.3533375}
}

@inproceedings{10.1145/3531130.3533375, 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. Among the various approaches to proofs in fixed-point logics, circular -- or cyclic -- proofs, are of interest in this regard but suffer from a number of limitations, most notably from a quite restricted use of cuts. Indeed, the validity condition which ensures soundness of non-wellfounded derivations and productivity of their cut-elimination prevents some computationally-relevant patterns of cuts. As a result, traditional circular proofs cannot serve as a basis for a theory of (co)recursive programming by lack of compositionality: there are not enough circular proofs and they compose badly. The present paper addresses some of these limitations by developing the circular and non-wellfounded proof-theory of multiplicative additive linear logic with fixed points () beyond the scope of the seminal works of Santocanale and Fortier and of Baelde et al. We define bouncing-validity: a new, generalized, validity criterion for , which takes axioms and cuts into account. We show soundness and cut elimination theorems for bouncing-valid non-wellfounded proofs: as a result, even though bouncing-validity proves the same sequents (or judgments) as before, we have many more valid proofs at our disposal. We illustrate the computational relevance of bouncing-validity on a number of examples. Finally, we study the decidability of the criterion in the circular case: we prove that it is undecidable in general but identify a hierarchy of decidable sub-criteria.}, Address = {New York, NY, USA}, Author = {Baelde, David and Doumane, Amina and Kuperberg, Denis and Saurin, Alexis}, BookTitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, File = {Bouncing Threads for Circular and Non-Wellfounded Proofs - 3531130.3533375.pdf}, ISBN = {9781450393515}, Keywords = {Linear Logic., Circular Proofs, Fixed Points, Curry-Howard, Coinduction, Decidability, Cut Elimination}, Location = {Haifa, Israel}, Publisher = {Association for Computing Machinery}, Series = {LICS '22}, Title = {Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs}, URL = {https://doi.org/10.1145/3531130.3533375}, Year = {2022}, articleno = {63}, bdsk-url-1 = {https://doi.org/10.1145/3531130.3533375}, date-added = {2022-08-29 14:27:27 +0200}, date-modified = {2022-08-29 14:27:27 +0200}, numpages = {13}, doi = {10.1145/3531130.3533375} }