A unification algorithm for typed -calculus

Cites work

A Complete Mechanization of Second-Order Type Theory
A formulation of the simple theory of types
A Machine-Oriented Logic Based on the Resolution Principle
Application à la viscoélasticité non linéaire du calcul symbolique à plusieurs variables
scientific article; zbMATH DE number 3349331 (Why is no real title available?)
scientific article; zbMATH DE number 3395450 (Why is no real title available?)
scientific article; zbMATH DE number 3412189 (Why is no real title available?)
scientific article; zbMATH DE number 3423994 (Why is no real title available?)
Mechanizing \(\omega\)-order type theory through unification
Resolution in type theory
The undecidability of unification in third order logic

Cited in

(58)

Finite generation of ambiguity in context-free languages
Theorem proving modulo
Completeness in PVS of a nominal unification algorithm
Middle-out reasoning for synthesis and induction
Evaluating lambda terms with traversals
Functions-as-constructors higher-order unification: extended pattern unification
The undecidability of proof search when equality is a logical connective
Restricted combinatory unification
Mechanized metatheory revisited
Types for modules
Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
Encoding generic judgments: preliminary results
The higher-order prover \textsc{Leo}-II
The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating English to FOL
Unification for -calculi without propagation rules
Regular patterns in second-order unification
Automatic theorem proving. II
Decidability of the unification problem for second-order languages with unary functional symbols
scientific article; zbMATH DE number 40567 (Why is no real title available?)
scientific article; zbMATH DE number 1231543 (Why is no real title available?)
Constraint handling rules with binders, patterns and generic quantification
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
Nominal unification with atom and context variables
Efficient full higher-order unification
Higher-order unification with dependent function types
Rewriting, and equational unification: the higher-order cases
Modular higher-order E-unification
Nominal Unification and Matching of Higher Order Expressions with Recursive Let
A matching process modulo a theory of categorical products
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
The practice of logical frameworks
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
Superposition with lambdas
Making higher-order superposition work
Superposition with lambdas
Superposition for higher-order logic
Higher order E-unification
Programming by example and proving by example using higher-order unification
The TPS theorem proving system
Representing unification in a logical framework
A Mizar mode for HOL
A type checker for a logical framework with union and intersection types (system description)
Efficient full higher-order unification
Pattern unification for the lambda calculus with linear and affine types
Refining unification with abstraction
A saturation-based unification algorithm for higher-order rational patterns
A higher-order Vampire (short paper)
Automated reasoning for mathematics
Canonical for automated theorem proving in Lean
Automating the derivation of unification algorithms. A case study in deductive program synthesis
Types, Tableaus and Gödel’s God in Isabelle/HOL
Strong Normalization of Moggis's Computational Metalanguage
TPS: A hybrid automatic-interactive system for developing proofs
Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited

This page was built for publication: A unification algorithm for typed \(\bar\lambda\)-calculus

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