A higher-order implementation of rewriting
From MaRDI portal
Publication:800739
DOI10.1016/0167-6423(83)90008-4zbMath0551.68076arXivcs/9301108WikidataQ57382757 ScholiaQ57382757MaRDI QIDQ800739
Publication date: 1983
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/cs/9301108
pattern matching; ML; formula conversions; implementation of rewriting in LCF; logic of computable functions; term conversions
68W30: Symbolic computation and algebraic computation
68Q65: Abstract data types; algebraic specification
03D60: Computability and recursion theory on ordinals, admissible sets, etc.
Related Items
A few exercises in theorem processing, Term rewriting and beyond -- theorem proving in Isabelle, Lazy techniques for fully expansive theorem proving, An overview of the Tecton proof system, Typed generic traversal with term rewriting strategies