Decidability of fourth-order matching

DOI10.1017/S0960129500003108MaRDI QIDQ4500172zbMATH OpenFDO

Authors Vincent Padovani

Publication date 14 February 2001

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129500003108

zbMATH Keywords

\(\lambda\)-calculusdecidabilityhigher order matchinghigher order unificationlambda-definability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1223619
• Higher-order beta matching with solutions in long beta-eta normal form
• Higher Order   Matching is Undecidable

Cited in

(16)

• Third order matching is decidable
• Decidability of bounded higher-order unification
• Nominal syntax with atom substitutions
• Model-checking games for typed -calculi
• Unification for -calculi without propagation rules
• Higher-order beta matching with solutions in long beta-eta normal form
• Dependency Tree Automata
• scientific article; zbMATH DE number 1223619 (Why is no real title available?)
• scientific article; zbMATH DE number 1341609 (Why is no real title available?)
• Third-order matching in the polymorphic lambda calculus
• Decidability of all minimal models
• Higher Order   Matching is Undecidable
• scientific article; zbMATH DE number 2090083 (Why is no real title available?)
• Computer Science Logic
• Automated Deduction – CADE-19
• Types, Tableaus and Gödel’s God in Isabelle/HOL

This page was built for publication: Decidability of fourth-order matching

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4500172)