Certifying Termination Proofs: From Term Rewriting to SMT Solving and Back (abstract)

A Fast Decision Procedure for Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems (abstract)

Strongly Normalizing Higher-Order Relational Queries (abstract)

WANDA - a Higher Order Termination Tool - System description (abstract)

Symbolic Execution Game Semantics (abstract)

A Probabilistic Higher-order Fixpoint Logic (abstract)

Refining Constructive Hybrid Games (abstract)

On Average-Case Hardness of Higher-Order Model Checking (abstract)

Adventures in Verifying Arithmetic (abstract)

A foundational lambda calculus for probabilistic computation (abstract)

Adaptive Non-linear Pattern Matching Automata (abstract)

Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars (abstract)

Unital Anti-unification: Type and Algorithms (abstract)

Undecidability of Semi-unification on a Napkin *** Best paper by a junior researcher (abstract)

Towards Constructive Hybrid Semantics (abstract)

String diagrams for optics (abstract)

A Profunctorial Scott Semantics (abstract)

Comprehension and quotient structures in the language of 2-categories (abstract)

Constraint Solving over Multiple Similarity Relations (abstract)

A Type Checker for a Logical Framework with Union and Intersection Types - System description (abstract)

Efficient Full Higher-Order Unification *** Best paper by junior researchers (abstract)

Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description (abstract)

Modules over monads and operational semantics (abstract)

Quotients in Dependent Type Theory (abstract)

Type safety of rewriting rules in dependent types (abstract)

Encoding Agda Programs using Rewriting (abstract)

The new rewriting engine of Dedukti - System description (abstract)

A Syntax for Mutual Inductive Families (abstract)

Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra (abstract)

Conditional Bisimilarity for Reactive Systems (abstract)

Resource-Aware Session Types with Arithmetic Refinements *** Best system description by a junior researcher (abstract)

Semi-Axiomatic Sequent Calculus (abstract)

A Gentzen-style monadic translation of Goedel's System T (abstract)

The difference lambda-calculus: a language for difference categories. (abstract)

A Reflection on Continuation-Composing Style (abstract)

Data-flow analyses as effects and graded monads (abstract)

A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers (abstract)

A Modal Analysis of Metaprogramming (abstract)