Higher-order unification with dependent function types

DOI10.1007/3-540-51081-8_104zbMath1503.68289OpenAlexW2113992680MaRDI QIDQ5055716

Conal M. Elliott

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-51081-8_104

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (13)

Higher-order unification, polymorphism, and subsorts ⋮ Higher-order unification via combinators ⋮ From programming-by-example to proving-by-example ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ The Alf proof editor and its proof engine ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ A combinatory logic approach to higher-order E-unification ⋮ An algorithm for checking incomplete proof objects in type theory with localization and unification ⋮ Unification under a mixed prefix ⋮ Proof-term synthesis on dependent-type systems via explicit substitutions ⋮ Elf: A meta-language for deductive systems ⋮ Proof-search in type-theoretic languages: An introduction ⋮ The practice of logical frameworks

Uses Software

• ML
• Miranda

Cites Work

• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Proofs of the normalization and Church-Rosser theorems for the typed \(\lambda\)-calculus
• A theory of type polymorphism in programming
• Proving and applying program transformations expressed with second-order patterns
• Higher-order unification revisited: Complete sets of transformations
• Uniform proofs as a foundation for logic programming
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Higher-order unification with dependent function types