Pages that link to "Item:Q5055716"
From MaRDI portal
The following pages link to Higher-order unification with dependent function types (Q5055716):
Displaying 25 items.
- Unifying sets and programs via dependent types (Q408534) (← links)
- A combinatory logic approach to higher-order E-unification (Q673971) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- Reduction and unification in lambda calculi with a general notion of subtype (Q1340967) (← links)
- A higher-order unification algorithm for inductive types and dependent types (Q1362142) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- A note on the proof theory of the \(\lambda \Pi\)-calculus (Q1891931) (← links)
- Higher-order unification via combinators (Q2367541) (← links)
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions (Q2480966) (← links)
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (Q4559809) (← links)
- An algorithm for checking incomplete proof objects in type theory with localization and unification (Q4647580) (← links)
- Higher-order superposition for dependent types (Q5055856) (← links)
- From programming-by-example to proving-by-example (Q5096230) (← links)
- Elf: A meta-language for deductive systems (Q5210815) (← links)
- Functions-as-constructors Higher-order Unification (Q5369491) (← links)
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (Q5372007) (← links)
- Theorem Proving in Higher Order Logics (Q5464654) (← links)
- The practice of logical frameworks (Q5878905) (← links)
- Higher-order unification, polymorphism, and subsorts (Q5881304) (← links)
- Proof-term synthesis on dependent-type systems via explicit substitutions (Q5958764) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
- The Alf proof editor and its proof engine (Q6083695) (← links)
- Investigations into proof-search in a system of first-order dependent function types (Q6488534) (← links)
- Programming by example and proving by example using higher-order unification (Q6488562) (← links)
- Representing unification in a logical framework (Q6560164) (← links)