Name
Abstract | ||
|---|---|---|
In this paper we study the constrained equivalence of programs with effects. In particular, we present a formal system for deriving such equivalences. The formal system we present defines a single-conclusion consequence relation between finite sets of constraints and assertions. Although the formal system is computationally adequate, even for expressions containing recursively defined functions, it is inadequate for proving properties of recursively defined functions. We show how to enrich the formal system by addition of induction principles. To illustrate the use of the formal system, we give three nontrivial examples of constrained equivalence assertions of well-known list-processing programs. We also establish several metatheoretic properties of constrained equivalence and the formal system, including soundness, completeness, and a comparison of the equivalence relations on various fragments. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1016/0304-3975(92)90301-U | Theor. Comput. Sci. |
Keywords | DocType | Volume |
functional program,mutate data | Journal | 105 |
Issue | ISSN | Citations |
2 | 0304-3975 | 17 |
PageRank | References | Authors |
1.65 | 14 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ian A. Mason | 1 | 797 | 97.47 |
| Carolyn Talcott | 2 | 1922 | 168.73 |