Abstract is missing.
- Compositional Confluence CriteriaKiraku Shintani, Nao Hirokawa. [doi]
- A Certified Algorithm for AC-UnificationMauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Daniele Nantes Sobrinho. [doi]
- On Lookaheads in Regular Expressions with BackreferencesNariyoshi Chida, Tachio Terauchi. [doi]
- Constructing Unprejudiced Extensional Type Theories with Choices via ModalitiesLiron Cohen 0001, Vincent Rahli. [doi]
- A Fibrational Tale of Operational Logical RelationsFrancesco Dagnino, Francesco Gavazzo. [doi]
- mwp-Analysis Improvement and Implementation: Realizing Implicit Computational ComplexityClément Aubert, Thomas Rubiano, Neea Rusch, Thomas Seiller. [doi]
- On Quantitative Algebraic Higher-Order TheoriesUgo Dal Lago, Furio Honsell, Marina Lenisa, Paolo Pistone. [doi]
- Addition and Differentiation of ZX-DiagramsEmmanuel Jeandel, Simon Perdrix, Margarita Veshchezerova. [doi]
- Sheaf Semantics of Termination-Insensitive NoninterferenceJonathan Sterling, Robert Harper. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Galois Connecting Call-by-Value and Call-by-NameDylan McDermott, Alan Mycroft. [doi]
- Stateful Structural Operational SemanticsSergey Goncharov 0001, Stefan Milius, Lutz Schröder, Stelios Tsampas 0001, Henning Urbat. [doi]
- Linear Lambda-Calculus is LinearAlejandro Díaz-Caro, Gilles Dowek. [doi]
- A Combinatorial Approach to Higher-Order Structure for Polynomial FunctorsMarcelo Fiore, Zeinab Galal, Hugo Paquet. [doi]
- Polynomial Termination Over ℕ Is UndecidableFabian Mitterwallner, Aart Middeldorp. [doi]
- Adequate and Computational Encodings in the Logical Framework DeduktiThiago Felicissimo. [doi]
- Division by Two, in Homotopy Type TheorySamuel Mimram, Émile Oleon. [doi]
- Rewriting for Monoidal Closed CategoriesMario Alvarez-Picallo, Dan R. Ghica, David Sprunger, Fabio Zanasi. [doi]
- A Stratified Approach to Löb InductionDaniel Gratzer, Lars Birkedal. [doi]
- A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk)Alwen Tiu. [doi]
- Certified Decision Procedures for Two-Counter MachinesAndrej Dudenhefner. [doi]
- Solvability for Generalized ApplicationsDelia Kesner, Loïc Peyrot. [doi]
- Decision Problems for Linear Logic with Least and Greatest Fixed PointsAnupam Das 0002, Abhishek De 0001, Alexis Saurin. [doi]
- Nominal Anti-Unification with Atom-VariablesManfred Schmidt-Schauß, Daniele Nantes Sobrinho. [doi]
- Type-Based Termination for FuturesSiva Somayyajula, Frank Pfenning. [doi]
- An Analysis of Tennenbaum's Theorem in Constructive Type TheoryMarc Hermes, Dominik Kirst. [doi]
- Combined Hierarchical Matching: the Regular CaseSerdar Erbatur, Andrew M. Marshall, Christophe Ringeissen. [doi]
- A Graphical Proof Theory of Logical TimeMatteo Acclavio, Ross Horne, Sjouke Mauw, Lutz Straßburger. [doi]
- Encoding Type Universes Without Using Matching Modulo Associativity and CommutativityFrédéric Blanqui. [doi]
- Normalization Without SyntaxWillem B. Heijltjes, Dominic J. D. Hughes, Lutz Straßburger. [doi]
- Strategies for Asymptotic NormalizationClaudia Faggian, Giulio Guerrieri. [doi]
- Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk)Cynthia Kop. [doi]
- Restricting Tree Grammars with Term RewritingJan Bessai, Lukasz Czajka 0001, Felix Laarmann, Jakob Rehof. [doi]