Operational and Semantic Equivalence Between Recursive Programs

DOI10.1145/322217.322229MaRDI QIDQ3893265zbMATH OpenOpenAlexFDO

Authors Jean Claude Raoult, Jean E. Vuillemin

Publication date 1980

Published in Journal of the ACM (Search for Journal in Brave)

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

zbMATH Keywords

algebraic semanticsfixed-point semanticsprogram equivalencerecursive programssemantics of programming languagessubtree replacement systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited in

(16)

• Termination of rewriting
• Full abstraction and limiting completeness in equational languages
• Graph grammars and operational semantics
• Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
• Conditional rewriting logic as a unified model of concurrency
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Some results on the confluence property of combined term rewriting systems
• Context-sensitive rewriting strategies
• Modularity in term rewriting revisited
• scientific article; zbMATH DE number 3896271 (Why is no real title available?)
• Total unfolding: theory and applications
• Algebraic semantics and complexity of term rewriting systems
• On modularity in term rewriting and narrowing
• Computing in unpredictable environments: Semantics, reduction strategies, and program transformations
• Semantics of non-terminating rewrite systems using minimal coverings
• Proving confluence in the confluence framework with confident

This page was built for publication: Operational and Semantic Equivalence Between Recursive Programs

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