Pages that link to "Item:Q1230505"
From MaRDI portal
The following pages link to A unification algorithm for typed \(\overline\lambda\)-calculus (Q1230505):
Displaying 50 items.
- Nominal abstraction (Q617715) (← links)
- A combinatory logic approach to higher-order E-unification (Q673971) (← links)
- Synthesis of rewrite programs by higher-order and semantic unification (Q749216) (← links)
- Simplifying the signature in second-order unification (Q843951) (← links)
- Expressing combinatory reduction systems derivations in the rewriting calculus (Q857913) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- On connections and higher-order logic (Q908896) (← links)
- A characterization of lambda definable tree operations (Q918191) (← links)
- Conditional equational theories and complete sets of transformations (Q918541) (← links)
- The calculus of context relations (Q918720) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- Word operation definable in the typed \(\lambda\)-calculus (Q1099156) (← links)
- Delaying unification algorithms for lambda calculi (Q1104776) (← links)
- A practically efficient and almost linear unification algorithm (Q1105360) (← links)
- The calculus of constructions (Q1108266) (← links)
- A unification algorithm for second-order monadic terms (Q1109019) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
- Polymorphic rewriting conserves algebraic strong normalization (Q1176244) (← links)
- Horn clause programs with polymorphic types: Semantics and resolution (Q1177936) (← links)
- Natural language syntax and first-order inference (Q1193491) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- A relaxation approach to splitting in an automatic theorem prover (Q1215411) (← links)
- A unification algorithm for typed \(\overline\lambda\)-calculus (Q1230505) (← links)
- Mechanizing \(\omega\)-order type theory through unification (Q1239309) (← links)
- The typed lambda-calculus is not elementary recursive (Q1259590) (← links)
- Unification with extended patterns (Q1274966) (← links)
- A decision algorithm for distributive unification (Q1275018) (← links)
- Unification problem in equational theories (Q1280985) (← links)
- Decidability of behavioural equivalence in unary PCF (Q1285665) (← links)
- Implementing tactics and tacticals in a higher-order logic programming language (Q1311396) (← links)
- A proof procedure for the logic of hereditary Harrop formulas (Q1311397) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- Third order matching is decidable (Q1337691) (← links)
- Reduction and unification in lambda calculi with a general notion of subtype (Q1340967) (← links)
- A semantics for \(\lambda \)Prolog (Q1349686) (← links)
- The Qu-Prolog unification algorithm: formalisation and correctness (Q1349886) (← links)
- A higher-order unification algorithm for inductive types and dependent types (Q1362142) (← links)
- Unification of infinite sets of terms schematized by primal grammars (Q1392278) (← links)
- Encoding transition systems in sequent calculus (Q1398474) (← links)
- Cut-elimination for a logic with definitions and induction (Q1575931) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- Nominal essential intersection types (Q1643145) (← links)
- Complete sets of unifiers and matchers in equational theories (Q1820760) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- On the logic of unification (Q1823935) (← links)
- Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
- The linked conjunct method for automatic deduction and related search techniques (Q1836998) (← links)
- Higher order unification via explicit substitutions (Q1854337) (← links)
- Decidability of bounded second order unification (Q1887168) (← links)
