Decidability of higher-order matching

Decidability of higher-order matching

We show that the higher-order matching problem is decidable using a game-theoretic argument.

Bibliographic Details
Main Author:	Colin Stirling
Format:	Article
Language:	English
Published:	Logical Methods in Computer Science e.V. 2009-07-01
Series:	Logical Methods in Computer Science
Subjects:	computer science - logic in computer science computer science - computer science and game theory f.4.1
Online Access:	https://lmcs.episciences.org/757/pdf

Similar Items

Petri Net Reachability Graphs: Decidability Status of First Order Properties
by: Philippe Darondeau, et al.
Published: (2012-10-01)

On the decidability and complexity of Metric Temporal Logic over finite words
by: Joel Ouaknine, et al.
Published: (2007-02-01)

Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy
by: Benjamin Bisping, et al.
Published: (2022-08-01)

The succinctness of first-order logic on linear orders
by: Martin Grohe, et al.
Published: (2005-06-01)

The Complexity of Model Checking Higher-Order Fixpoint Logic
by: Roland Axelsson, et al.
Published: (2007-06-01)

Two-Variable Logic with Two Order Relations
by: Thomas Schwentick, et al.
Published: (2012-03-01)

On the Parameterized Intractability of Monadic Second-Order Logic
by: Stephan Kreutzer
Published: (2012-03-01)

A note on the expressive power of linear orders
by: Thomas Schwentick, et al.
Published: (2011-12-01)

Algorithms for Omega-Regular Games with Imperfect Information
by: Krishnendu Chatterjee, et al.
Published: (2007-07-01)

Realizability algebras: a program to well order R
by: Jean-Louis Krivine
Published: (2011-08-01)

Successor-Invariant First-Order Logic on Classes of Bounded Degree
by: Julien Grange
Published: (2021-08-01)

The monadic second-order logic of graphs XVI : Canonical graph decompositions
by: Bruno Courcelle
Published: (2006-03-01)

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
by: Assia Mahboubi, et al.
Published: (2012-02-01)

Deciding Kleene Algebras in Coq
by: Thomas Braibant, et al.
Published: (2012-03-01)

O-Minimal Hybrid Reachability Games
by: Patricia Bouyer, et al.
Published: (2010-01-01)

On the First-Order Complexity of Induced Subgraph Isomorphism
by: Oleg Verbitsky, et al.
Published: (2019-03-01)

A Characterisation of First-Order Constraint Satisfaction Problems
by: Benoit Larose, et al.
Published: (2007-11-01)

Lindstrom theorems for fragments of first-order logic
by: Johan van Benthem, et al.
Published: (2009-08-01)

On Second-Order Monadic Monoidal and Groupoidal Quantifiers
by: Juha Kontinen, et al.
Published: (2010-09-01)

Formalizing Randomized Matching Algorithms
by: Dai Tri Man Le, et al.
Published: (2012-08-01)

Positional Determinacy of Games with Infinitely Many Priorities
by: Erich Graedel, et al.
Published: (2006-11-01)

A note on first-order spectra with binary relations
by: Eryk Kopczynski, et al.
Published: (2018-04-01)

First-order query evaluation on structures of bounded degree
by: Wojciech Kazana, et al.
Published: (2011-06-01)

Fixed point combinators as fixed points of higher-order fixed point generators
by: Andrew Polonsky
Published: (2020-07-01)

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
by: Sanjit A. Seshia, et al.
Published: (2005-12-01)

Exhaustible sets in higher-type computation
by: Martin Escardo
Published: (2008-08-01)

The Algebraic Intersection Type Unification Problem
by: Andrej Dudenhefner, et al.
Published: (2017-08-01)

No solvable lambda-value term left behind
by: Á. García-Pérez, et al.
Published: (2016-06-01)

Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL
by: L. Nenzi, et al.
Published: (2018-10-01)

Mixin Composition Synthesis based on Intersection Types
by: Jan Bessai, et al.
Published: (2018-02-01)

Axioms for Modelling Cubical Type Theory in a Topos
by: Ian Orton, et al.
Published: (2018-12-01)

A proof system for graph (non)-isomorphism verification
by: Milan Banković, et al.
Published: (2023-02-01)

Bounded Linear Logic, Revisited
by: Ugo Dal Lago, et al.
Published: (2010-12-01)

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
by: Federico Aschieri, et al.
Published: (2010-09-01)

The Omega Rule is $\mathbf{\Pi_{1}^{1}}$-Complete in the $\lambda\beta$-Calculus
by: Benedetto Intrigila, et al.
Published: (2009-04-01)

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
by: Andreas Abel, et al.
Published: (2011-05-01)

Formalising the pi-calculus using nominal logic
by: Jesper Bengtson, et al.
Published: (2009-06-01)

Comparing hierarchies of total functionals
by: Dag Normann
Published: (2005-10-01)

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
by: Jose Espirito Santo, et al.
Published: (2009-05-01)

The Independence of Markov's Principle in Type Theory
by: Thierry Coquand, et al.
Published: (2017-08-01)