A unification algorithm for typed \(\bar\lambda\)-calculus
From MaRDI portal
Publication:1227601
DOI10.1016/0304-3975(75)90011-0zbMath0332.02035OpenAlexW2034676877MaRDI QIDQ1227601
Publication date: 1975
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(75)90011-0
Related Items
Set-of-support strategy for higher-order logic, Higher-order unification, polymorphism, and subsorts, Second-order unification in the presence of linear shallow algebraic equations, The higher-order prover \textsc{Leo}-II, Functions-as-constructors higher-order unification: extended pattern unification, The undecidability of proof search when equality is a logical connective, The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL, Types for modules, Higher-order unification with dependent function types, Regular Patterns in Second-Order Unification, Rewriting, and equational unification: the higher-order cases, Modular higher-order E-unification, Unification for $$\lambda $$ -calculi Without Propagation Rules, Nominal Unification and Matching of Higher Order Expressions with Recursive Let, TPS: A hybrid automatic-interactive system for developing proofs, Finite generation of ambiguity in context-free languages, Middle-out reasoning for synthesis and induction, A matching process modulo a theory of categorical products, Unnamed Item, Constraint handling rules with binders, patterns and generic quantification, Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited, Superposition for higher-order logic, Automatic theorem proving. II, Unnamed Item, Theorem proving modulo, Unnamed Item, Completeness in PVS of a nominal unification algorithm, An algorithm for checking incomplete proof objects in type theory with localization and unification, On intuitionistic proof nets with additional rewrite rules and their approximations, The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations, Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions, Evaluating lambda terms with traversals, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Unnamed Item, Superposition with lambdas, Making higher-order superposition work, Superposition with lambdas, Decidability of the unification problem for second-order languages with unary functional symbols, Restricted combinatory unification, Mechanized metatheory revisited, Encoding Generic Judgments, The practice of logical frameworks
Cites Work
- Mechanizing \(\omega\)-order type theory through unification
- Application à la viscoélasticité non linéaire du calcul symbolique à plusieurs variables
- A Machine-Oriented Logic Based on the Resolution Principle
- Resolution in type theory
- A Complete Mechanization of Second-Order Type Theory
- The undecidability of unification in third order logic
- A formulation of the simple theory of types
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
