ON THE AXIOMATIZATION OF 'IF-THEN-ELSE'.

Irene Guessarian, Jose Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)332-357
Number of pages26
JournalSIAM Journal on Computing
Volume16
Issue number2
DOIs
StatePublished - Jan 1 1987
Externally publishedYes

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'ON THE AXIOMATIZATION OF 'IF-THEN-ELSE'.'. Together they form a unique fingerprint.

Cite this