A logic programming language with lambda-abstraction, function variables, and simple unification

DOI10.1007/BFB0038698MaRDI QIDQ5053011zbMATH OpenOpenAlexFDO

Authors

Publication date 26 November 2022

Published in Extensions of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bfb0038698

Mathematics Subject Classification ID

Logic programming (68N17) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• scientific article; zbMATH DE number 4180832
• A treatment of higher-order features in logic programming
• scientific article; zbMATH DE number 3872643
• Programming with higher-order logic.

Cited in

(29)

• Higher order disunification: some decidable cases
• Problems in rewriting III
• Existential type systems between Church and Curry style (type-free style)
• A theory of binding structures and applications to rewriting
• Higher order conditional rewriting and narrowing
• Higher-ranked annotation polymorphic dependency analysis
• Inductive-data-type systems
• Higher-order families
• Higher-order annotated terms for proof search
• Higher-order proof by consistency
• Context rewriting
• Rewriting, and equational unification: the higher-order cases
• scientific article; zbMATH DE number 2090550 (Why is no real title available?)
• scientific article; zbMATH DE number 3942988 (Why is no real title available?)
• Higher order unification via explicit substitutions
• Normalisation for higher-order calculi with explicit substitutions
• Developing developments
• scientific article; zbMATH DE number 970726 (Why is no real title available?)
• Cut elimination for a logic with induction and co-induction
• A treatment of higher-order features in logic programming
• Representing proof transformations for program optimization
• Decidable higher-order unification problems
• Automated Reasoning
• Higher-order superposition for dependent types
• scientific article; zbMATH DE number 3872643 (Why is no real title available?)
• ELPI: fast, embeddable, Prolog interpreter
• A restricted form of higher-order rewriting applied to an HDL semantics
• Middle-out reasoning for synthesis and induction
• Constraint handling rules with binders, patterns and generic quantification

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 Q5053011)