| 2023 | The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic. | Thomas Ehrhard, Claudia Faggian, Michele Pagani |
| 2023 | Quotients and Extensionality in Relational Doctrines. | Francesco Dagnino, Fabio Pasquali |
| 2023 | Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach. | Serenella Cerrito, Valentin Goranko, Sophie Paillocher |
| 2023 | Unifying Graded Linear Logic and Differential Operators. | Flavien Breuvart, Marie Kerjean, Simon Mirwasser |
| 2023 | For the Metatheory of Type Theory, Internal Sconing Is Enough. | Rafal Bocquet, Ambrus Kaposi, Christian Sattler |
| 2023 | Diller-Nahm Bar Recursion. | Valentin Blot |
| 2023 | Strategies as Resource Terms, and Their Categorical Semantics. | Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair |
| 2023 | Convolution Products on Double Categories and Categorification of Rule Algebras. | Nicolas Behr, Paul-Andr Mellis, Noam Zeilberger |
| 2023 | Concurrent Realizability on Conjunctive Structures. | Emmanuel Beffara, Flix Castro, Mauricio Guillermo, tienne Miquey |
| 2023 | Two Decreasing Measures for Simply Typed λ-Terms. | Pablo Barenbaum, Cristian Sottile |
| 2023 | Combinatory Logic and Lambda Calculus Are Equal, Algebraically. | Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tams Vgh |
| 2023 | Cyclic Proofs for Arithmetical Inductive Definitions. | Anupam Das, Lukas Melgaard |
| 2023 | Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). | Akihisa Yamada |
| 2023 | Representing Guardedness in Call-By-Value. | Sergey Goncharov |
| 2022 | Front Matter, Table of Contents, Preface, Conference Organization. | |
| 2022 | A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk). | Alwen Tiu |
| 2022 | Sheaf Semantics of Termination-Insensitive Noninterference. | Jonathan Sterling, Robert Harper |
| 2022 | Type-Based Termination for Futures. | Siva Somayyajula, Frank Pfenning |
| 2022 | Compositional Confluence Criteria. | Kiraku Shintani, Nao Hirokawa |
| 2022 | Nominal Anti-Unification with Atom-Variables. | Manfred Schmidt-Schau, Daniele Nantes-Sobrinho |
| 2022 | Polynomial Termination Over ℕ Is Undecidable. | Fabian Mitterwallner, Aart Middeldorp |
| 2022 | Division by Two, in Homotopy Type Theory. | Samuel Mimram, mile Oleon |
| 2022 | Galois Connecting Call-by-Value and Call-by-Name. | Dylan McDermott, Alan Mycroft |
| 2022 | On Quantitative Algebraic Higher-Order Theories. | Ugo Dal Lago, Furio Honsell, Marina Lenisa, Paolo Pistone |
| 2022 | Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk). | Cynthia Kop |