Abstract is missing.
- String Diagrams for OpticsGuillaume Boisseau. [doi]
- Comprehension and Quotient Structures in the Language of 2-CategoriesPaul-André Melliès, Nicolas Rolland. [doi]
- Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description)Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi. [doi]
- The New Rewriting Engine of Dedukti (System Description)Gabriel Hondet, Frédéric Blanqui. [doi]
- Undecidability of Semi-Unification on a NapkinAndrej Dudenhefner. [doi]
- Modules over Monads and Operational SemanticsAndré Hirschowitz, Tom Hirschowitz, Ambroise Lafont. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Constraint Solving over Multiple Similarity RelationsBesik Dundua, Temur Kutsia, Mircea Marin, Cleopatra Pau. [doi]
- Solvability in a Probabilistic Setting (Invited Talk)Simona Ronchi Della Rocca, Ugo Dal Lago, Claudia Faggian. [doi]
- A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting SystemsMasaomi Yamaguchi, Takahito Aoto 0001. [doi]
- Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree GrammarsKazuyuki Asada, Naoki Kobayashi 0001. [doi]
- A Type Checker for a Logical Framework with Union and Intersection Types (System Description)Claude Stolze, Luigi Liquori. [doi]
- A Profunctorial Scott SemanticsZeinab Galal. [doi]
- The Difference λ-Calculus: A Language for Difference CategoriesMario Alvarez-Picallo, C.-H. Luke Ong. [doi]
- A Syntax for Mutual Inductive FamiliesAmbrus Kaposi, Jakob von Raumer. [doi]
- Conditional Bisimilarity for Reactive SystemsMathias Hülsbusch, Barbara König 0001, Sebastian Küpper, Lars Stoltenow. [doi]
- WANDA - a Higher Order Termination Tool (System Description)Cynthia Kop. [doi]
- Encoding Agda Programs Using RewritingGuillaume Genestier. [doi]
- A Probabilistic Higher-Order Fixpoint LogicYo Mitani, Naoki Kobayashi 0001, Takeshi Tsukada. [doi]
- A Complete Normal-Form Bisimilarity for Algebraic Effects and HandlersDariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. [doi]
- Unital Anti-Unification: Type and AlgorithmsDavid M. Cerna, Temur Kutsia. [doi]
- Quotients in Dependent Type Theory (Invited Talk)Andrew M. Pitts. [doi]
- Symbolic Execution Game SemanticsYu-Yang Lin, Nikos Tzevelekos. [doi]
- Refining Constructive Hybrid GamesBrandon Bohrer, André Platzer. [doi]
- Efficient Full Higher-Order UnificationPetar Vukmirovic, Alexander Bentkamp, Visa Nummelin. [doi]
- Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene AlgebraPaul Brunet, David J. Pym. [doi]
- Semi-Axiomatic Sequent CalculusHenry DeYoung, Frank Pfenning, Klaas Pruiksma. [doi]
- Certifying the Weighted Path Order (Invited Talk)René Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada 0002. [doi]
- Data-Flow Analyses as Effects and Graded MonadsAndrej Ivaskovic, Alan Mycroft, Dominic Orchard. [doi]
- Type Safety of Rewrite Rules in Dependent TypesFrédéric Blanqui. [doi]
- A Gentzen-Style Monadic Translation of Gödel's System TChuangjie Xu. [doi]
- A Reflection on Continuation-Composing StyleDariusz Biernacki, Mateusz Pyzik, Filip Sieczkowski. [doi]
- Towards Constructive Hybrid SemanticsTim Lukas Diezel, Sergey Goncharov 0001. [doi]
- A Modal Analysis of Metaprogramming, Revisited (Invited Talk)Brigitte Pientka. [doi]
- Adaptive Non-Linear Pattern Matching AutomataRick Erkens, Maurice Laveaux. [doi]
- Strongly Normalizing Higher-Order Relational QueriesWilmer Ricciotti, James Cheney. [doi]
- Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description)Ankush Das, Frank Pfenning. [doi]
- On Average-Case Hardness of Higher-Order Model CheckingYoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi 0001, Ryoma Sin'ya, Takeshi Tsukada. [doi]