Pages that link to "Item:Q3985547"
From MaRDI portal
The following pages link to A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification (Q3985547):
Displaying 50 items.
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
- An initial algebra approach to term rewriting systems with variable binders (Q853743) (← 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)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited (Q894695) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Capture-avoiding substitution as a nominal algebra (Q939160) (← links)
- A polynomial nominal unification algorithm (Q944382) (← links)
- A domain model characterising strong normalisation (Q958484) (← links)
- Matching and alpha-equivalence check for nominal terms (Q980937) (← links)
- Abstract deduction and inferential models for type theory (Q988551) (← links)
- Deterministic second-order patterns (Q1029104) (← links)
- On the algebraic structure of declarative programming languages (Q1035699) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- Unification with extended patterns (Q1274966) (← 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)
- Reduction and unification in lambda calculi with a general notion of subtype (Q1340967) (← links)
- A semantics for \(\lambda \)Prolog (Q1349686) (← links)
- Correspondences between classical, intuitionistic and uniform provability (Q1575924) (← links)
- Efficient resource management for linear logic proof search (Q1575929) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- Higher-order substitutions (Q1854398) (← links)
- Nominal unification (Q1882909) (← links)
- Logical approximation for program analysis (Q1929363) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Higher-order pattern anti-unification in linear time (Q2362208) (← links)
- Types for modules (Q2375744) (← links)
- Decidability of bounded higher-order unification (Q2456577) (← links)
- Tractable and intractable second-order matching problems (Q2643530) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Case Analysis of Higher-Order Data (Q2804942) (← links)
- Encoding Generic Judgments (Q2841234) (← links)
- (Q2851046) (← links)
- Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions (Q2866332) (← links)
- Redundancy Elimination for LF (Q2871840) (← links)
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming (Q2875221) (← links)
- A Library of Anti-unification Algorithms (Q2938520) (← links)
- Normal Higher-Order Termination (Q2946769) (← links)
- The First-Order Nominal Link (Q3003496) (← links)
- A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains (Q3010373) (← links)
- A proof-theoretic treatment of <i>λ</i>-reduction with cut-elimination: <i>λ</i>-calculus as a logic programming language (Q3011126) (← links)
- Cooperation of Algebraic Constraint Domains in Higher-Order Functional and Logic Programming (Q3067475) (← links)
- Term Sequent Logic (Q4982627) (← links)
- (Q4993338) (← links)
