Pages that link to "Item:Q1227601"

The following pages link to A unification algorithm for typed \(\bar\lambda\)-calculus (Q1227601):

Displaying 46 items.

• The higher-order prover \textsc{Leo}-II (Q287283) (← links)
• TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
• Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited (Q894695) (← links)
• Finite generation of ambiguity in context-free languages (Q1117043) (← links)
• Theorem proving modulo (Q1431339) (← links)
• Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
• Middle-out reasoning for synthesis and induction (Q1915136) (← links)
• Evaluating lambda terms with traversals (Q2007730) (← links)
• Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
• The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
• Restricted combinatory unification (Q2305407) (← links)
• Mechanized metatheory revisited (Q2323447) (← links)
• Types for modules (Q2375744) (← links)
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions (Q2480966) (← links)
• Encoding generic judgments: preliminary results (Q2841234) (← links)
• The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL (Q2900507) (← links)
• Unification for $$\lambda $$ -calculi Without Propagation Rules (Q3179400) (← links)
• Regular Patterns in Second-Order Unification (Q3454122) (← links)
• Automatic theorem proving. II (Q3793764) (← links)
• Decidability of the unification problem for second-order languages with unary functional symbols (Q3885741) (← links)
• The connection between the fundamental groupoid and a unification algorithm for syntactic algebras (Extended abstract) (Q3994022) (← links)
• (Q4222859) (← links)
• Constraint handling rules with binders, patterns and generic quantification (Q4592722) (← links)
• An algorithm for checking incomplete proof objects in type theory with localization and unification (Q4647580) (← links)
• On intuitionistic proof nets with additional rewrite rules and their approximations (Q4916174) (← links)
• The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations (Q4916200) (← links)
• Nominal unification with atom and context variables (Q4993360) (← links)
• (Q5028439) (← links)
• Higher-order unification with dependent function types (Q5055716) (← links)
• Rewriting, and equational unification: the higher-order cases (Q5055746) (← links)
• Modular higher-order E-unification (Q5055760) (← links)
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let (Q5075515) (← links)
• A matching process modulo a theory of categorical products (Q5096201) (← links)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic (Q5191100) (← links)
• The practice of logical frameworks (Q5878905) (← links)
• Set-of-support strategy for higher-order logic (Q5881215) (← links)
• Higher-order unification, polymorphism, and subsorts (Q5881304) (← links)
• Second-order unification in the presence of linear shallow algebraic equations (Q5881305) (← links)
• Superposition with lambdas (Q5918381) (← links)
• Making higher-order superposition work (Q5918575) (← links)
• Superposition with lambdas (Q5919500) (← links)
• Superposition for higher-order logic (Q6156638) (← links)
• Higher order E-unification (Q6488561) (← links)
• Programming by example and proving by example using higher-order unification (Q6488562) (← links)
• Representing unification in a logical framework (Q6560164) (← links)
• A Mizar mode for HOL (Q6567713) (← links)