| 2021 | A Strong Call-By-Need Calculus. | Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond |
| 2021 | Abstract Clones for Abstract Syntax. | Nathanael Arkor, Dylan McDermott |
| 2021 | New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial. | Anupam Das, Alex A. Rice |
| 2021 | On the Logical Strength of Confluence and Normalisation for Cyclic Proofs. | Anupam Das |
| 2021 | An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems. | Dohan Kim, Christopher Lynch |
| 2020 | A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems. | Masaomi Yamaguchi, Takahito Aoto |
| 2020 | A Gentzen-Style Monadic Translation of Gdel's System T. | Chuangjie Xu |
| 2020 | Front Matter, Table of Contents, Preface, Conference Organization. | |
| 2020 | Efficient Full Higher-Order Unification. | Petar Vukmirovic, Alexander Bentkamp, Visa Nummelin |
| 2020 | Certifying the Weighted Path Order (Invited Talk). | Ren Thiemann, Jonas Schpf, Christian Sternagel, Akihisa Yamada |
| 2020 | A Type Checker for a Logical Framework with Union and Intersection Types (System Description). | Claude Stolze, Luigi Liquori |
| 2020 | Solvability in a Probabilistic Setting (Invited Talk). | Simona Ronchi Della Rocca, Ugo Dal Lago, Claudia Faggian |
| 2020 | Strongly Normalizing Higher-Order Relational Queries. | Wilmer Ricciotti, James Cheney |
| 2020 | Quotients in Dependent Type Theory (Invited Talk). | Andrew M. Pitts |
| 2020 | A Modal Analysis of Metaprogramming, Revisited (Invited Talk). | Brigitte Pientka |
| 2020 | On Average-Case Hardness of Higher-Order Model Checking. | Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada |
| 2020 | A Probabilistic Higher-Order Fixpoint Logic. | Yo Mitani, Naoki Kobayashi, Takeshi Tsukada |
| 2020 | Comprehension and Quotient Structures in the Language of 2-Categories. | Paul-Andr Mellis, Nicolas Rolland |
| 2020 | Symbolic Execution Game Semantics. | Yu-Yang Lin, Nikos Tzevelekos |
| 2020 | WANDA - a Higher Order Termination Tool (System Description). | Cynthia Kop |
| 2020 | A Syntax for Mutual Inductive Families. | Ambrus Kaposi, Jakob von Raumer |
| 2020 | Data-Flow Analyses as Effects and Graded Monads. | Andrej Ivaskovic, Alan Mycroft, Dominic Orchard |
| 2020 | Conditional Bisimilarity for Reactive Systems. | Mathias Hlsbusch, Barbara Knig, Sebastian Kpper, Lara Stoltenow |
| 2020 | The New Rewriting Engine of Dedukti (System Description). | Gabriel Hondet, Frdric Blanqui |
| 2020 | Modules over Monads and Operational Semantics. | Andr Hirschowitz, Tom Hirschowitz, Ambroise Lafont |