Operational and Semantic Equivalence Between Recursive Programs

DOI10.1145/322217.322229zbMath0447.68004OpenAlexW2070558135MaRDI QIDQ3893265

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 semanticsrecursive programsprogram equivalencefixed-point semanticssemantics of programming languagessubtree replacement systems

Mathematics Subject Classification ID

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

Related Items

Some results on the confluence property of combined term rewriting systems ⋮ Algebraic semantics and complexity of term rewriting systems ⋮ Termination of rewriting ⋮ Full abstraction and limiting completeness in equational languages ⋮ On modularity in term rewriting and narrowing ⋮ Modularity in term rewriting revisited ⋮ Graph grammars and operational semantics ⋮ Rewrite, rewrite, rewrite, rewrite, rewrite, \dots ⋮ Conditional rewriting logic as a unified model of concurrency ⋮ Unnamed Item ⋮ Confluence of the lambda calculus with left-linear algebraic rewriting ⋮ Context-sensitive rewriting strategies ⋮ Total unfolding: theory and applications ⋮ Computing in unpredictable environments: Semantics, reduction strategies, and program transformations

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