Contributions to Proceedings:
F. Schernhammer, J. Meseguer:
"Incremental Checking of Well-Founded Recursive Specifications Modulo Axioms";
in: "Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2011), July 20-22, 2011, Odense, Denmark",
P. Schneider-Kamp, M. Hanus (ed.);
issued by: Peter Schneider-Kamp and Michael Hanus;
We introduce the notion of well-founded recursive order-sorted
equational logic (OS) theories modulo axioms. Such theories define
functions by well-founded recursion and are inherently terminating.
Moreover, for well-founded recursive theories important properties
such as confluence and sufficient completeness are modular
for so-called fair extensions. This enables us to incrementally check
these properties for hierarchies of such theories that occur naturally
in modular rule-based functional programs. Well-founded recursive
OS theories modulo axioms contain only commutativity and
associativity-commutativity axioms. In order to support arbitrary
combinations of associativity, commutativity and identity axioms,
we show how to eliminate identity and (under certain conditions)
associativity (without commutativity) axioms by theory transformations
in the last part of the paper.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.