Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity

Frédéric Blanqui

Solvability for Generalized Applications

Delia Kesner and Loïc Peyrot

Polynomial Termination over N Is Undecidable

Fabian Mitterwallner and Aart Middeldorp

Normalization Without Syntax

Willem Heijltjes, Dominic Hughes and Lutz Straßburger

An Analysis of Tennenbaum's Theorem in Constructive Type Theory

Marc Hermes and Dominik Kirst

Certified Decision Procedures for Two-Counter Machines

Andrej Dudenhefner

Type-Based Termination for Futures

Siva Somayyajula and Frank Pfenning

Constructing Unprejudiced Extensional Type Theories with Choices via Modalities

Liron Cohen and Vincent Rahli

Galois Connecting Call-by-Value and Call-by-Name

Dylan McDermott and Alan Mycroft

A Fibrational Tale of Operational Logical Relations

Francesco Dagnino and Francesco Gavazzo

Nominal anti-Unification with Atom-Variables

Manfred Schmidt-Schauss and Daniele Nantes-Sobrinho

Mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity

Clément Aubert, Thomas Rubiano, Neea Rusch and Thomas Seiller

Division by Two, in Homotopy Type Theory

Samuel Mimram and Émile Oleon

Addition and Differentiation of ZX-Diagrams

Margarita Veshchezerova, Emmanuel Jeandel and Simon Perdrix

Combined Hierarchical Matching: the Regular Case

Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen

On Quantitative Algebraic Higher-Order Theories

Ugo Dal Lago, Furio Honsell, Marina Lenisa and Paolo Pistone

On Lookaheads in Regular Expressions with Backreferences

Nariyoshi Chida and Tachio Terauchi

A Certified Algorithm for AC-Unification

Mauricio Ayala-Rincón, Maribel Fernandez, Gabriel Ferreira Silva and Daniele Nantes-Sobrinho

Linear Lambda-Calculus Is Linear

Alejandro Díaz-Caro and Gilles Dowek

Sheaf Semantics of Termination-Insensitive Noninterference

Jonathan Sterling and Robert Harper