Accepted Papers

  • Homotopy type theory as internal languages of diagrams of $\infty$-logoses – Taichi Uemura. 
  • The Formal Theory of Monads, Univalently – Niels van der Weide. 
  • Automata-based verification of relational properties of functions over data structures – Théo Losekoot, Thomas Genet and Thomas Jensen. 
  • The Sum-Product Algorithm for Quantitative Multiplicative Linear Logic – Michele Pagani, Thomas Ehrhard and Claudia Faggian. 
  • Generalized Newman’s Lemma for Discrete and Continuous Systems – Ievgen Ivanov. 
  • E-unification for Second-Order Abstract Syntax – Nikolai Kudasov. 
  • Two Decreasing Measures for Simply Typed Lambda-Terms – Pablo Barenbaum and Cristian Sottile. 
  • Hydra Battles and AC Termination – Nao Hirokawa and Aart Middeldorp. 
  • Strategies as Resource Terms, and their Categorical Semantics – Lison Blondeau-Patissier, Pierre Clairambault and Lionel Vaux Auclair. 
  • Rewriting modulo traced comonoid structure – Dan Ghica and George Kaye. 
  • Cost-Size Semantics for Call-by-Value Higher-Order Rewriting – Deivid Vale and Cynthia Kop. 
  • Categorical coherence from term rewriting systems – Samuel Mimram. 
  • Convolution Products on Double Categorie and Categorification of Rule Algebras – Nicolas Behr, Paul-André Melliès and Noam Zeilberger. 
  • For the Metatheory of Type Theory, Internal Sconing Is Enough – Rafaël Bocquet, Ambrus Kaposi and Christian Sattler. 
  • The logical essence of compiling with continuations – José Espírito Santo and Filipa Mendes. 
  • On the Lattice of Program Metrics – Ugo Dal Lago, Naohiko Hoshino and Paolo Pistone. 
  • Unifying Graded Linear Logic and Differential Operators – Flavien Breuvart, Marie Kerjean and Simon Mirwasser. 
  • α-avoidance – Samuel Frontull, Georg Moser and Vincent van Oostrom. 
  • Partial model checking and partial model synthesis in LTL using a tableau-based approach – Serenella Cerrito, Valentin Goranko and Sophie Paillocher. 
  • Combinatory logic and lambda calculus are equal, algebraically – Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs and Tamás Végh. 
  • Quotients and Extensionality in Relational Doctrines – Francesco Dagnino and Fabio Pasquali. 
  • Type Isomorphisms for Multiplicative Additive Linear Logic – Rémi Di Guardia and Olivier Laurent. 
  • Cyclic proofs for (arithmetical) inductive definitions – Anupam Das and Lukas Melgaard. 
  • Concurrent Realizability on Conjunctive Structures – Emmanuel Beffara, Félix Castro, Mauricio Guillermo and Étienne Miquey. 
  • A quantitative version of simple types – Simona Ronchi Della Rocca and Daniele Pautasso. 
  • Knowledge Problems in Security Protocols: Going Beyond Subterm-Convergent – Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen. 
  • Labelled Tableaux for Linear Time Bunched Implication Logic – Didier Galmiche and Daniel Mery. 
  • Diller-Nahm bar recursion – Valentin Blot. 
  • Dinaturality meets genericity: a game semantics of bounded polymorphism. – James Laird. 
  • Representing Guardedness in Call-by-Value – Sergey Goncharov.