3 papers
cs.LO2026
Staying Productive Under the Palm Trees: On Graded Coeffect Typing in the Tropical Semiring
Rémy Cerda, Rémy Cerda, Ugo Dal Lago
We show that the tropical semiring over the natural numbers, when used as the grading space in graded coeffect typing, faithfully models the passage of time while simultaneously gu…
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…