TY - GEN
T1 - On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
AU - Meseguer, José
AU - Skeirik, Stephen
N1 - Publisher Copyright:
© 2022, Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - Both complete definition of functions by equations and determinism (i.e., evaluation to a unique result), are fundamental correctness properties of equational programs. But for expressive functional languages supporting conditional equations, types and subtypes and rewriting modulo axioms, proof methods for verifying such properties under general conditions are currently quite limited. This work proposes a hierarchical proof methodology where both properties are simultaneously verified in a hierarchical manner under termination assumptions.
AB - Both complete definition of functions by equations and determinism (i.e., evaluation to a unique result), are fundamental correctness properties of equational programs. But for expressive functional languages supporting conditional equations, types and subtypes and rewriting modulo axioms, proof methods for verifying such properties under general conditions are currently quite limited. This work proposes a hierarchical proof methodology where both properties are simultaneously verified in a hierarchical manner under termination assumptions.
UR - http://www.scopus.com/inward/record.url?scp=85135871024&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85135871024&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-12441-9_10
DO - 10.1007/978-3-031-12441-9_10
M3 - Conference contribution
AN - SCOPUS:85135871024
SN - 9783031124402
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 191
EP - 211
BT - Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
A2 - Bae, Kyungmin
PB - Springer
T2 - 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Y2 - 2 April 2022 through 3 April 2022
ER -