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

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Logic programming (68N17) 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

(32)

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

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)