The equationally complete proof system for 'if-then-else' of S. Bloom and R. Tindell is extended to a complete proof system for many-sorted algebras with extra operations, predicates and equations among those. We give similar completeness results for continuous algebras and program schemes (infinite trees) by the methods of algebraic semantics. These extensions provide a purely equational proof system to prove properties of functional programs over user-definable data types.
ASJC Scopus subject areas
- Computer Science(all)