Abstract: The purpose of this paper is threefold. First, we describe some basic ideas of constructive type theory, with emphasis on their value for specification. Second, we demonstrate the use of type theory as a specification language. This is done by means of a detailed example, namely, the specification of an abstract data type (ADT) for multisets. Finally, we describe how a theorem proving environment built on type theory can be used to aid in implementation of the ADT.
Previous | Index | Next An error occured whilst processing this directive