A higher-order implementation of rewriting
From MaRDI portal
Publication:800739
DOI10.1016/0167-6423(83)90008-4zbMath0551.68076arXivcs/9301108OpenAlexW1636139685WikidataQ57382757 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 matchingMLformula conversionsimplementation of rewriting in LCFlogic of computable functionsterm conversions
Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65) Computability and recursion theory on ordinals, admissible sets, etc. (03D60)
Related Items
An overview of the Tecton proof system, Rewriting conversions implemented with continuations, Crystal: Integrating structured queries into a tactic language, A few exercises in theorem processing, A metatheory of a mechanized object theory, Typed generic traversal with term rewriting strategies, Term rewriting and beyond -- theorem proving in Isabelle, Scalable fine-grained proofs for formula processing, Equational Reasoning with Applicative Functors, Generic type-preserving traversal strategies, REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS, Lazy techniques for fully expansive theorem proving, Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
