FSCD 2025 Accepted Papers

Ievgen Ivanov. Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality
Andrej Dudenhefner. Mechanized Undecidability of Higher-order beta-Matching
Samuel Mimram and Emile Oleon. Coherent Tietze transformations of 1-polygraphs in homotopy type theory
Dilian Gurov and Reiner Hähnle. An Expressive Trace Logic for Recursive Programs
Elies Harington and Samuel Mimram. ∞-categorical models of linear logic
Thomas Traversié. Monad Translations for Higher-Order Logic
Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot and Matthieu Piquerez. A Zoo of Continuity Properties in Constructive Type Theory
Marie Kerjean, Valentin Maestracci and Morgan Rogers. Functorial Models of Differential Linear Logic
Franz Baader and Oliver Fernández Gil. The Unification Type of an Equational Theory May Depend on the Instantiation Preorder
Carsten Fuhs, Liye Guo and Cynthia Kop. An Innermost DP Framework for Constrained Higher-order Rewriting
Luc Passemard, Uli Fahrenberg and Amazigh Amrane. Higher-Dimensional Automata : Extension to Infinite Tracks
Sergei Stepanenko and Amin Timany. Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
Meven Lennon-Bertrand. What does it take to certify a conversion checker?
Emmanuel Hainry, Romain Péchoux and Mário Silva. Branch Sequentialization in Quantum Polytime
Willem Heijltjes. Quantitative Types for the Functional Machine Calculus
Rémy Cerda, Giulio Manzonetto and Alexis Saurin. Memory trees and Taylor expansion for the λI-calculus
Liron Cohen, Ariel Grunfeld, Dominik Kirst, Étienne Miquey and Ross Tate. From Partial to Monadic: Combinatory Algebra with Effects
Dale Miller. Linear logic using negative connectives
Martín Escardó, Bruno da Rocha Paiva, Vincent Rahli and Ayberk Tosun. Internal Effectful Forcing in System T
Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl and Joost-Pieter Katoen. Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation
Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora De Falco and Lionel Vaux Auclair. Yeo’s Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
Serdar Erbatur, Andrew M. Marshall, Paliath Narendran and Christophe Ringeissen. Knowledge Problems vs Unification and Matching: Dichotomy Results
Flavien Breuvart and Hugo Paquet. Categorical Continuation Semantics for Concurrency
Bapstiste Chanus, Damiano Mazza and Morgan Rogers. Unifying Algebraic and Boolean Descriptive Complexity
Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot and Claudio Sacerdoti Coen. The Cost of Skeletal Call-by-Need, Smoothly
C. B. Aberlé, Chris Martens and Frank Pfenning. Substructural Parametricity
Steven Bronsveld, Herman Geuvers and Niels van der Weide. Impredicative Encodings of Inductive and Coinductive Types
Ugo Dal Lago, Naohiko Hoshino and Paolo Pistone. On the Metric Nature of (Differential) Logical Relations
Dylan McDermott. Grading call-by-push-value, explicitly and implicitly
Mauricio Ayala-Rincón, David Cerna, Temur Kutsia and Christophe Ringeissen. Combining Generalization Algorithms in Regular Collapse-Free Theories