Higher-order unification with dependent function types
From MaRDI portal
Recommendations
- A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
- Unification in an extensional lambda calculus with ordered function sorts and constant overloading
- A higher-order unification algorithm for inductive types and dependent types
- Higher-order unification via combinators
- Higher-order dynamic pattern unification for dependent types and records
Cites work
- scientific article; zbMATH DE number 3878393 (Why is no real title available?)
- scientific article; zbMATH DE number 3951980 (Why is no real title available?)
- scientific article; zbMATH DE number 4051039 (Why is no real title available?)
- scientific article; zbMATH DE number 4053062 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- A framework for defining logics
- A theory of type polymorphism in programming
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Higher-order unification revisited: Complete sets of transformations
- Proofs of the normalization and Church-Rosser theorems for the typed \(\lambda\)-calculus
- Proving and applying program transformations expressed with second-order patterns
- The undecidability of the second-order unification problem
- Uniform proofs as a foundation for logic programming
Cited in
(35)- Unifying Sets and Programs via Dependent Types
- Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach
- The practice of logical frameworks
- Hints in Unification
- Higher-order unification, polymorphism, and subsorts
- Representing unification in a logical framework
- Unifying sets and programs via dependent types
- Programming by example and proving by example using higher-order unification
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- Higher-order dynamic pattern unification for dependent types and records
- Unification in an extensional lambda calculus with ordered function sorts and constant overloading
- scientific article; zbMATH DE number 1512625 (Why is no real title available?)
- Higher-order unification via combinators
- Unified syntax with iso-types
- Tableaux for automated reasoning in dependently-typed higher-order logic
- Theorem Proving in Higher Order Logics
- A unification algorithm for Coq featuring universe polymorphism and overloading
- scientific article; zbMATH DE number 1670734 (Why is no real title available?)
- The Alf proof editor and its proof engine
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- scientific article; zbMATH DE number 1678369 (Why is no real title available?)
- A note on the proof theory of the -calculus
- Reduction and unification in lambda calculi with a general notion of subtype
- Unification under a mixed prefix
- Higher-order superposition for dependent types
- Investigations into proof-search in a system of first-order dependent function types
- From programming-by-example to proving-by-example
- Elf: A meta-language for deductive systems
- Proof-search in type-theoretic languages: An introduction
- Proof-term synthesis on dependent-type systems via explicit substitutions
- Functions-as-constructors Higher-order Unification
- A combinatory logic approach to higher-order E-unification
- An algorithm for checking incomplete proof objects in type theory with localization and unification
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
- A Survey of the Proof-Theoretic Foundations of Logic Programming
This page was built for publication: Higher-order unification with dependent function types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055716)
