2 papers
cs.LO2026
Compression for Coinductive Rewriting and the Cut-Elimination of Non-Wellfounded Proofs
Rémy Cerda, Rémy Cerda, Alexis Saurin
We introduce a generic presentation of "syntactic objects built by mixed induction and coinduction" encompassing all standard kinds of infinitary terms, as well as derivation trees…
cs.LO2026
Ohana trees, linear approximation and multi-types for the I-calculus: No variable gets left behind or forgotten!
Rémy Cerda, Giulio Manzonetto, Alexis Saurin
Although the I-calculus is a natural fragment of the -calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The…