| 2024 | Simulating Dependency Pairs by Semantic Labeling. | Teppei Saito, Nao Hirokawa |
| 2024 | State Canonization and Early Pruning in Width-Based Automated Theorem Proving. | Mateus de Oliveira Oliveira, Farhad Vadiee |
| 2024 | Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories. | Ralph Matthes, Kobe Wullaert, Benedikt Ahrens |
| 2024 | Termination of Generalized Term Rewriting Systems. | Salvador Lucas |
| 2024 | Meaningfulness and Genericity in a Subsuming Framework (Invited Talk). | Delia Kesner, Victor Arrial, Giulio Guerrieri |
| 2024 | Laplace Distributors and Laplace Transformations for Differential Categories. | Marie Kerjean, Jean-Simon Pacaud Lemay |
| 2024 | Two-Dimensional Kripke Semantics I: Presheaves. | Georgios Alexandros Kavvos |
| 2024 | Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. | Ambrus Kaposi, Szumi Xie |
| 2024 | Representation of Peano Arithmetic in Separation Logic. | Sohei Ito, Makoto Tatsuta |
| 2024 | On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice Principles. | Hugo Herbelin, Jad Koleilat |
| 2024 | Machine-Checked Categorical Diagrammatic Reasoning. | Benot Guillemet, Assia Mahboubi, Matthieu Piquerez |
| 2024 | A Categorical Approach to DIBI Models. | Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, Fabio Zanasi |
| 2024 | Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. | Thiago Felicissimo, Tho Winterhalter |
| 2024 | Bhm and Taylor for All! | Alos Dufour, Damiano Mazza |
| 2024 | Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. | Andrej Dudenhefner, Daniele Pautasso |
| 2024 | Automating Boundary Filling in Cubical Agda. | Maximilian Dor, Evan Cavallo, Anders Mrtberg |
| 2024 | The Flower Calculus. | Pablo Donato |
| 2024 | homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. | Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, Jamie Vicary |
| 2024 | Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. | Kostia Chardonnet, Louis Lemonnier, Benot Valiron |
| 2024 | Delooping Generated Groups in Homotopy Type Theory. | Camil Champin, Samuel Mimram, mile Oleon |
| 2024 | Abstraction-Based Decision Making for Statistical Properties (Invited Talk). | Filip Cano, Thomas A. Henzinger, Bettina Knighofer, Konstantin Kueffner, Kaushik Mallik |
| 2024 | Optimizing a Non-Deterministic Abstract Machine with Environments. | Malgorzata Biernacka, Dariusz Biernacki, Sergue Lenglet, Alan Schmitt |
| 2024 | On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. | Franz Baader, Jrgen Giesl |
| 2024 | Mirroring Call-By-Need, or Values Acting Silly. | Beniamino Accattoli, Adrienne Lancelot |
| 2024 | IMELL Cut Elimination with Linear Overhead. | Beniamino Accattoli, Claudio Sacerdoti Coen |