Abstract
The aim of this paper is to model recursive types, equational types, and elementary programming control constructs (such as conditionals and while-do) in one, comparatively simple, algebraic framework, that can be used for theoretical studies and as a basis for data type and program specification. To this end we introduce a new kind of algebraic theory, the RV-theory. We give simple examples of the use of such theories for data type specification. We provide a mathematical semantics for these specifications that extends the initial algebra semantics for equational specification to include recursive types.
Get full access to this article
View all access options for this article.