Higher-order term indexing using substitution trees

DOI10.1145/1614431.1614437MaRDI QIDQ2946592zbMATH OpenOpenAlexFDO

Authors Brigitte Pientka

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1614431.1614437

zbMATH Keywords

type theorylogical frameworksindexing

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Logic Programming
• Term indexing
• Substitution tree indexing
• scientific article; zbMATH DE number 1552512
• Advanced indexing operations on substitution trees

Cited in

(12)

• Logic Programming
• Restricted combinatory unification
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Higher-order pattern anti-unification in linear time
• Term indexing
• Advanced indexing operations on substitution trees
• Higher-order pattern generalization modulo equational theories
• One or nothing: anti-unification over the simply-typed lambda calculus
• scientific article; zbMATH DE number 7455734 (Why is no real title available?)
• A Generic Framework for Higher-Order Generalizations.
• Higher-order equational pattern anti-unification
• There is no best \(\beta \)-normalization strategy for higher-order reasoners

Describes a project that uses

Uses Software

• Twelf

This page was built for publication: Higher-order term indexing using substitution trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946592)