A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
From MaRDI portal
Recommendations
- A logic programming language with lambda-abstraction, function variables, and simple unification
- scientific article; zbMATH DE number 3872643
- A treatment of higher-order features in logic programming
- MLOG: A strongly typed confluent functional language with logical variables
- scientific article; zbMATH DE number 970726
Cited in
(only showing first 100 items - show all)- Deterministic second-order patterns
- On the algebraic structure of declarative programming languages
- Higher-order rewrite systems and their confluence
- Unification under a mixed prefix
- Unification with extended patterns
- Implementing tactics and tacticals in a higher-order logic programming language
- A proof procedure for the logic of hereditary Harrop formulas
- MLOG: A strongly typed confluent functional language with logical variables
- Reduction and unification in lambda calculi with a general notion of subtype
- A semantics for Prolog
- Correspondences between classical, intuitionistic and uniform provability
- Efficient resource management for linear logic proof search
- Introduction to ``Milestones in interactive theorem proving
- Higher-order substitutions
- Nominal unification
- Logical approximation for program analysis
- Functions-as-constructors higher-order unification: extended pattern unification
- The undecidability of proof search when equality is a logical connective
- From LCF to Isabelle/HOL
- Mechanized metatheory revisited
- Higher-order pattern anti-unification in linear time
- Types for modules
- Decidability of bounded higher-order unification
- Tractable and intractable second-order matching problems
- Extensional higher-order paramodulation in Leo-III
- Case analysis of higher-order data
- Encoding generic judgments: preliminary results
- Rewriting calculus with(out) types
- Functional programming with higher-order abstract syntax and explicit substitutions
- Redundancy elimination for LF
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming
- A library of anti-unification algorithms
- Normal higher-order termination
- The First-Order Nominal Link
- A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
- A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
- Cooperation of algebraic constraint domains in higher-order functional and logic programming
- Scoping constructs in logic programming: Implementation problems and their solution
- A consistent extension of the lambda-calculus as a base for functional programming languages
- scientific article; zbMATH DE number 3872643 (Why is no real title available?)
- On the Relation between Sized-Types Based Termination and Semantic Labelling
- scientific article; zbMATH DE number 3942988 (Why is no real title available?)
- Size-based termination of higher-order rewriting
- CLP(\(\mathsf{H}\)): constraint logic programming for hedges
- Development closed critical pairs
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- The suspension notation for lambda terms and its use in metalanguage implementations
- Term sequent logic
- Higher-order equational pattern anti-unification
- Nominal unification with atom and context variables
- Linear unification of higher-order patterns
- A logic programming language with lambda-abstraction, function variables, and simple unification
- A termination ordering for higher order rewrite systems
- Higher-order narrowing with definitional trees
- Linear second-order unification
- Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
- Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
- Nominal Unification and Matching of Higher Order Expressions with Recursive Let
- A Generic Framework for Higher-Order Generalizations.
- scientific article; zbMATH DE number 7566074 (Why is no real title available?)
- Modular AC unification of higher-order patterns
- Higher-order narrowing with convergent systems
- How to prove decidability of equational theories with second-order computation analyser SOL
- Higher-order pattern generalization modulo equational theories
- The CADE-26 automated theorem proving system competition -- CASC-26
- A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains
- Automated Reasoning
- Rewriting and Call-Time Choice: The HO Case
- Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
- scientific article; zbMATH DE number 970726 (Why is no real title available?)
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- The practice of logical frameworks
- Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
- Superposition with lambdas
- Superposition with lambdas
- Higher-order matching for program transformation
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
- A logical framework with higher-order rational (circular) terms
- Nominal anti-unification modulo equational theories
- Wanda -- a higher-order termination tool (system description)
- The new rewriting engine of dedukti (system description)
- Encoding Agda programs using rewriting
- Mechanized metatheory revisited: an extended abstract (invited paper)
- Equational reasoning modulo commutativity in languages with binders
- The computability path order for beta-eta-normal higher-order rewriting
- Impredicativity, cumulativity and product covariance in the logical framework dedukti
- Rewriting modulo in the -calculus Modulo
- Adelfa: a system for reasoning about LF specifications
- Pattern unification for the lambda calculus with linear and affine types
- A saturation-based unification algorithm for higher-order rational patterns
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Two applications of logic programming to Coq
- Semantics of pattern unification
- An initial algebra approach to term rewriting systems with variable binders
- Expressing combinatory reduction systems derivations in the rewriting calculus
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- TPS: A hybrid automatic-interactive system for developing proofs
- Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
This page was built for publication: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3985547)
