Data abstraction in programming language semantics

Most modern programming languages allow the user to define abstract data types, thereby creating an extended language. While the programming language without the definition of ADT\u27s is completely described by its operational semantics, the new constants in the extended language need to be specified in some appropriate formalism. Algebraic equations are one such formalism; such a specification of an ADT constrains the class of valid implementations of the ADT by requiring that the equations be observational equivalences in the extended language. To reason about the extended language it is useful to have a denotational semantics. This thesis studies the denotational semantics of languages with algebraically specified ADT\u27s. For a natural class of models for the extended language we give a necessary and sufficient condition for a model to be computationally adequate with respect to the extended language. This is shown in a variety of language settings--in particular, for a variant of call-by-name PCF, called $PCF\sb{n}$, and a variant of call-by-value PCF, called $PCF\sb{v\sp-}$ to show the general nature of the ideas. We define a class of algebras called reachable, fully abstract algebras, and exhibit a general construction that for a given algebraic specification of an ADT and any fully abstract algebra satisfying the specification constructs a fully abstract model of $PCF\sb{n}$ extended with the ADT. This construction is rather syntactic, and so we consider some special cases where a semantic construction of a fully abstract model can be carried out. We then show the construction of two reachable, fully abstract algebras satisfying the specification. Both these algebras have appealing categorical descriptions that can be used to define paradigms of specification semantics, similar to initial and final algebra semantics. For any programming language, there is the problem of reasoning about its models. Mechanization of such reasoning is intractable, in general, and therefore it is useful to consider specific fragments. We consider a fragment of $PCF\sb{n}$ extended with ADT\u27s that consists of simply typed lambda terms with algebraic constants. We study certain natural axiomatizations of specific environment models, which are models of call by name lambda calculi, and derive sufficient conditions for their completeness