"Quotient relations and data abstraction"

Abstract

So-called logical relations are used to model the idea that some programs act abstractly. They provide some of the strongest mathematics in the semantics of computation. Indeed the subject is fraught with open questions. We illustrate the basic ideas with an application to data abstraction developed by Power and Robinson. We then describe a special class of relations called quotient relations. These are motivated by a naive model of data abstraction and are often adequate where more general relations have been used. We emphasize the intuitions behind the abstract results.