A characterisation of computable data types by means of a finite, equational specification method : (preprint)
Jan Aldert Bergstra, John Vivian Tucker · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1979
Within the framework of the ADJ Group's algebraic theory of data types, we are able to give a characterisation of those data types and data structures whose semantics are constructive in terms of the structural properties of algebraically styled "proof systems" available for their definition.It is proved that the computable data types are precisely those which may be defined by deductive systems, equationally specified in a finite way, and which satisfy two simple conditions on the deductions which may take place within them.