Dmitriy Traytel . Formal Languages, Formally and Coinductively Olivier Laurent . Focusing in Orthologic Stefan Kahrs and Connor Smith. Non-omega-overlapping TRSs are UN Tomer Libal and Dale Miller . Functions-as-constructors Higher-order Unification Franziska Rapp and Aart Middeldorp . Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground TRSs
Martin Avanzini and Georg Moser . Complexity of Term Graph Rewriting Ofer Arieli and Arnon Avron . Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency Thorsten Altenkirch and Ambrus Kaposi . Normalisation by Evaluation for Dependent Types Ryota Akiyoshi and Kazushige Terui . Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule Takahito Aoto and Yoshihito Toyama . Ground Confluence Prover based on Rewriting Induction Thierry Coquand and Bassel Mannaa . The Independence of Markov’s Principle in Type Theory Andrej Dudenhefner , Jakob Rehof and Moritz Martens. The Intersection Type Unification Problem Cynthia Kop and Jakob Grue Simonsen . Complexity Hierarchies and Higher-Order Cons-Free Rewriting
Marcin Benke, Aleksy Schubert and Daria Walukiewicz-Chrząszcz. Synthesis of Functional Programs with Help of First-order Intuitionistic Logic
Kaustuv Chaudhuri , Sonia Marin and Lutz Strassburger . Modular Focused Proof Systems for Intuitionistic Modal Logics Andrés Aristizábal, Dariusz Biernacki , Sergueï Lenglet and Piotr Polesiuk. Environmental bisimulations for delimited-control operators with dynamic prompt generation
Flavien Breuvart , Giulio Manzonetto , Andrew Polonsky and Domenico Ruoppolo . New Results on Morris's Observational Theory: the benefits of separating the inseparable Fer-Jan de Vries . On Undefined and Meaningless in Lambda Definability Stéphane Gimenez and David Obwaller. Interaction Automata and the ia2d Interpreter Giulio Guerrieri , Luc Pellissier and Lorenzo Tortora De Falco . Computing connected proof(-structure)s from their Taylor expansion Vincent van Oostrom and Yoshihito Toyama. Normalisation by Random Descent
Naoki Nishida , Adrian Palacios and German Vidal . Reversible Term Rewriting Amin Timany and Bart Jacobs . Category Theory in Coq 8.5
Philippe Malbos and Samuel Mimram . Homological Computations for Term Rewriting Systems Jon Hael Brenas, Rachid Echahed and Martin Strecker . Proving Correctness of Graph Rewriting Systems using C2PDL
Christian Sternagel and Thomas Sternagel . Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata CompletionValentin Blot . Classical extraction in continuation models James Laird . Weighted Relational Models for Mobile Names Krzysztof Bar, Aleks Kissinger and Jamie Vicary. Globular: a proof assistant for higher rewriting
Daniele Nantes-Sobrinho , Mauricio Ayala-Rincon and Maribel Fernandez . Nominal Narrowing Makoto Hamana . Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theory Ryuta Arisaka. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus