Recommendations
Cites work
- scientific article; zbMATH DE number 3878393 (Why is no real title available?)
- scientific article; zbMATH DE number 4053062 (Why is no real title available?)
- scientific article; zbMATH DE number 65531 (Why is no real title available?)
- scientific article; zbMATH DE number 1158760 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 3999882 (Why is no real title available?)
- A Complete Mechanization of Second-Order Type Theory
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A unification algorithm for typed -calculus
- Completeness in the theory of types
- General models and extensionality
- Higher-order Horn clauses
- Higher-order unification revisited: Complete sets of transformations
- Higher-order unification with dependent function types
- Intuitionistic propositional logic is polynomial-space complete
- Mechanizing \(\omega\)-order type theory through unification
- Natural deduction as higher-order resolution
- On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
- Proving and applying program transformations expressed with second-order patterns
- Resolution in type theory
- The foundation of a generic theorem prover
- The undecidability of the second-order unification problem
- The undecidability of unification in third order logic
Cited in
(34)- Reasoning in Abella about structural operational semantics specifications
- Higher order disunification: some decidable cases
- A colored version of the \(\lambda\)-calculus
- Third-order matching in the polymorphic lambda calculus
- Higher-Order Multi-Valued Resolution
- On extensibility of proof checkers
- Mechanized metatheory revisited
- Functions-as-constructors higher-order unification: extended pattern unification
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Unification with extended patterns
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Nominal abstraction
- Hybrid linear logic, revisited
- Hilbert's epsilon as an operator of indefinite committed choice
- Recasting ML\(^{\text F}\)
- Verifying termination and reduction properties about higher-order logic programs
- Higher order unification via explicit substitutions
- Set theory for verification. I: From foundations to functions
- Types for modules
- On the role of names in reasoning about \(\lambda\)-tree syntax specifications
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- COCHIS: stable and coherent implicits
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Third order matching is decidable
- A proof procedure for the logic of hereditary Harrop formulas
- A two-level logic approach to reasoning about computations
- Implementing tactics and tacticals in a higher-order logic programming language
- Translating higher-order clauses to first-order clauses
- Implementing type theory in higher order constraint logic programming
- The undecidability of proof search when equality is a logical connective
- Proof-term synthesis on dependent-type systems via explicit substitutions
- Tactics and parameters
- A Survey of the Proof-Theoretic Foundations of Logic Programming
This page was built for publication: Unification under a mixed prefix
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1201348)
