ion is one of the pillars of computer science . Of course . choosing the right concept s to emphasize, and details to suppress, is crucial in all of science, but in computer science th e role of abstraction extends beyond that of sensible methodology . For in computing we have see n the emergence of an array of constructs and methods whose chief purpose is to provide genera l mechanisms for achieving, validating, or enforcing abstraction, rather than being specific instances or examples of it . Among these are programming concepts such as objects . procedures, abstract data types and modules, and mathematical methods such as simulation and logical relations .But what, more precisely, is the "abstraction " achieved by these constructs? In the case o f procedural abstraction, a more or less satisfactory explanation can be given in terms of functions . Much more subtle, and novel, is the idea of data abstraction : A collection of programs or operations conspiring together to represent higher level pieces of data .What kind of mathematical entities are data abstractions? One answer is provided by algebra , and there has been a good deal of development of the theory of algebraic specifications . This theory is important, but it does not provide a comprehensive answer . In particular . it does no t cope comfortably with imperative or object-oriented features, with the ability to generate ne w abstractions (as in new objects), and it is limited to first-order functions .The purpose of this article is to trace a line of development which revolves around a cor e calculus, the polymorphic A-calculus of Girard [6] and Reynolds . Just as the A-calculus is th e Β©Peter W .