On Ground Convergence and Completeness of Conditional Equational Program Hierarchies

José Meseguer; Stephen Skeirik

doi:10.1007/978-3-031-12441-9_10

On Ground Convergence and Completeness of Conditional Equational Program Hierarchies

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English (US)
Title of host publication	Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
Editors	Kyungmin Bae
Publisher	Springer
Pages	191-211
Number of pages	21
ISBN (Print)	9783031124402
DOIs	https://doi.org/10.1007/978-3-031-12441-9_10
State	Published - 2022
Externally published	Yes
Event	14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 - Munich, Germany Duration: Apr 2 2022 → Apr 3 2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13252 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Country/Territory	Germany
City	Munich
Period	4/2/22 → 4/3/22

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-031-12441-9_10

Library availability

Discover UIUC Full Text

Cite this

Meseguer, J., & Skeirik, S. (2022). On Ground Convergence and Completeness of Conditional Equational Program Hierarchies. In K. Bae (Ed.), Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers (pp. 191-211). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13252 LNCS). Springer. https://doi.org/10.1007/978-3-031-12441-9_10

On Ground Convergence and Completeness of Conditional Equational Program Hierarchies. / Meseguer, José; Skeirik, Stephen.
Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. ed. / Kyungmin Bae. Springer, 2022. p. 191-211 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13252 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Meseguer, J & Skeirik, S 2022, On Ground Convergence and Completeness of Conditional Equational Program Hierarchies. in K Bae (ed.), Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13252 LNCS, Springer, pp. 191-211, 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022, Munich, Germany, 4/2/22. https://doi.org/10.1007/978-3-031-12441-9_10

Meseguer J, Skeirik S. On Ground Convergence and Completeness of Conditional Equational Program Hierarchies. In Bae K, editor, Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. Springer. 2022. p. 191-211. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-12441-9_10

Meseguer, José ; Skeirik, Stephen. / On Ground Convergence and Completeness of Conditional Equational Program Hierarchies. Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. editor / Kyungmin Bae. Springer, 2022. pp. 191-211 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9fea005b87604033baf8b0771b8ddea5,

title = "On Ground Convergence and Completeness of Conditional Equational Program Hierarchies",

abstract = "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.",

author = "Jos{\'e} Meseguer and Stephen Skeirik",

note = "Publisher Copyright: {\textcopyright} 2022, Springer Nature Switzerland AG.; 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 ; Conference date: 02-04-2022 Through 03-04-2022",

year = "2022",

doi = "10.1007/978-3-031-12441-9_10",

language = "English (US)",

isbn = "9783031124402",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "191--211",

editor = "Kyungmin Bae",

booktitle = "Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers",

address = "Germany",

}

TY - GEN

T1 - On Ground Convergence and Completeness of Conditional Equational Program Hierarchies

AU - Meseguer, José

AU - Skeirik, Stephen

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 -