A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
From MaRDI portal
Publication:3985547
DOI10.1093/logcom/1.4.497zbMath0738.68016DBLPjournals/logcom/Miller91OpenAlexW2075352622WikidataQ64216211 ScholiaQ64216211MaRDI QIDQ3985547
No author found.
Publication date: 27 June 1992
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1607&context=cis_reports
quantificationunification algorithmcorrectness of interpretationcorrectness of unificationrestricted \(\beta\)-conversionuntyped unification and interpretation
Related Items (83)
Higher-order pattern anti-unification in linear time ⋮ Nominal unification ⋮ Linear unification of higher-order patterns ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ The undecidability of proof search when equality is a logical connective ⋮ Reduction and unification in lambda calculi with a general notion of subtype ⋮ Types for modules ⋮ A termination ordering for higher order rewrite systems ⋮ Linear second-order unification ⋮ Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type ⋮ A semantics for \(\lambda \)Prolog ⋮ Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ An initial algebra approach to term rewriting systems with variable binders ⋮ Tractable and intractable second-order matching problems ⋮ Expressing combinatory reduction systems derivations in the rewriting calculus ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ A Library of Anti-unification Algorithms ⋮ Size-based termination of higher-order rewriting ⋮ Higher-order rewrite systems and their confluence ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Normal Higher-Order Termination ⋮ Modular AC unification of higher-order patterns ⋮ Higher-order narrowing with convergent systems ⋮ Logical approximation for program analysis ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ CLP(H):Constraint logic programming for hedges ⋮ Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited ⋮ A logical framework with higher-order rational (circular) terms ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Higher-order pattern generalization modulo equational theories ⋮ Decidability of bounded higher-order unification ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Capture-avoiding substitution as a nominal algebra ⋮ The First-Order Nominal Link ⋮ A polynomial nominal unification algorithm ⋮ A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains ⋮ A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language ⋮ Development closed critical pairs ⋮ Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules ⋮ A domain model characterising strong normalisation ⋮ Unification under a mixed prefix ⋮ The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations ⋮ Unnamed Item ⋮ A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains ⋮ Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) ⋮ Matching and alpha-equivalence check for nominal terms ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ Abstract deduction and inferential models for type theory ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ Higher-order matching for program transformation ⋮ Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions ⋮ Cooperation of Algebraic Constraint Domains in Higher-Order Functional and Logic Programming ⋮ Case Analysis of Higher-Order Data ⋮ Rewriting and Call-Time Choice: The HO Case ⋮ Superposition with lambdas ⋮ Nominal Unification from a Higher-Order Perspective ⋮ Superposition with lambdas ⋮ A Generic Framework for Higher-Order Generalizations. ⋮ Unification with extended patterns ⋮ On the Relation between Sized-Types Based Termination and Semantic Labelling ⋮ Term Sequent Logic ⋮ Deterministic second-order patterns ⋮ On the algebraic structure of declarative programming languages ⋮ Mechanized metatheory revisited ⋮ Encoding Generic Judgments ⋮ Correspondences between classical, intuitionistic and uniform provability ⋮ Efficient resource management for linear logic proof search ⋮ Higher-order substitutions ⋮ Implementing tactics and tacticals in a higher-order logic programming language ⋮ A proof procedure for the logic of hereditary Harrop formulas ⋮ 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 ⋮ Higher-order narrowing with definitional trees ⋮ The practice of logical frameworks ⋮ Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
Uses Software
This page was built for publication: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
