Abstract is missing.
- Category Theory in Coq 8.5Amin Timany, Bart Jacobs 0002. [doi]
- Coalgebras and Higher-Order Computation: a GoI ApproachIchiro Hasuo. [doi]
- Nominal NarrowingMauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes Sobrinho. [doi]
- Non-Omega-Overlapping TRSs are UNStefan Kahrs, Connor Smith. [doi]
- Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite SystemsFranziska Rapp, Aart Middeldorp. [doi]
- Classical Extraction in Continuation ModelsValentin Blot. [doi]
- Homological Computations for Term Rewriting SystemsPhilippe Malbos, Samuel Mimram. [doi]
- The Intersection Type Unification ProblemAndrej Dudenhefner, Moritz Martens, Jakob Rehof. [doi]
- Complexity Hierarchies and Higher-Order Cons-Free RewritingCynthia Kop, Jakob Grue Simonsen. [doi]
- On Undefined and Meaningless in Lambda DefinabilityFer-Jan de Vries. [doi]
- The Independence of Markov's Principle in Type TheoryThierry Coquand, Bassel Mannaa. [doi]
- Complexity of Acyclic Term Graph RewritingMartin Avanzini, Georg Moser. [doi]
- Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory FormalizationGérard Huet. [doi]
- Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee [doi]
- Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.Ryota Akiyoshi, Kazushige Terui. [doi]
- Minimal Paradefinite Logics for Reasoning with Incompleteness and InconsistencyOfer Arieli, Arnon Avron. [doi]
- Reversible Term RewritingNaoki Nishida 0001, Adrián Palacios, Germán Vidal. [doi]
- Computing Connected Proof(-Structure)s From Their Taylor ExpansionGiulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco. [doi]
- Functions-as-Constructors Higher-Order UnificationTomer Libal, Dale Miller. [doi]
- Verified Analysis of Functional Data StructuresTobias Nipkow. [doi]
- Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic TheoriesMakoto Hamana. [doi]
- Proving Correctness of Logically Decorated Graph Rewriting SystemsJon Haël Brenas, Rachid Echahed, Martin Strecker. [doi]
- Modular Focused Proof Systems for Intuitionistic Modal LogicsKaustuv Chaudhuri, Sonia Marin, Lutz Straßburger. [doi]
- New Results on Morris's Observational Theory: The Benefits of Separating the InseparableFlavien Breuvart, Giulio Manzonetto, Andrew Polonsky, Domenico Ruoppolo. [doi]
- Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt GenerationAndrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. [doi]
- Interaction Automata and the ia2d InterpreterStéphane Gimenez, David Obwaller. [doi]
- Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata CompletionChristian Sternagel, Thomas Sternagel. [doi]
- Synthesis of Functional Programs with Help of First-Order Intuitionistic LogicMarcin Benke, Aleksy Schubert, Daria Walukiewicz-Chrzaszcz. [doi]
- Weighted Relational Models for MobilityJames Laird. [doi]
- Focusing in OrthologicOlivier Laurent. [doi]
- Formal Languages, Formally and CoinductivelyDmitriy Traytel. [doi]
- Compositional Compiler Verification for a Multi-Language WorldAmal Ahmed. [doi]
- Structural Interactions and Absorption of Structural Rules in BI Sequent CalculusRyuta Arisaka. [doi]
- Globular: An Online Proof Assistant for Higher-Dimensional RewritingKrzysztof Bar, Aleks Kissinger, Jamie Vicary. [doi]
- Ground Confluence Prover based on Rewriting InductionTakahito Aoto 0001, Yoshihito Toyama. [doi]
- Normalisation by Evaluation for Dependent TypesThorsten Altenkirch, Ambrus Kaposi. [doi]
- Normalisation by Random DescentVincent van Oostrom, Yoshihito Toyama. [doi]