On Ground Convergence and Completeness of Conditional Equational Program Hierarchies

José Meseguer, Stephen Skeirik

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
EditorsKyungmin Bae
PublisherSpringer
Pages191-211
Number of pages21
ISBN (Print)9783031124402
DOIs
StatePublished - 2022
Externally publishedYes
Event14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 - Munich, Germany
Duration: Apr 2 2022Apr 3 2022

Publication series

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

Conference

Conference14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Country/TerritoryGermany
CityMunich
Period4/2/224/3/22

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'On Ground Convergence and Completeness of Conditional Equational Program Hierarchies'. Together they form a unique fingerprint.

Cite this