Simple Type-Theoretic Foundations for Object-Oriented Programming：（面向对象编程简单Type-Theoretic基础）.pdfVIP

c J Functional Programming 1 January Cambridge University Press Simple TypeTheoretic Foundations For ObjectOriented Programming Benjamin C Pierce David N Turner Department of Computer Science University of Edinburgh The Kings Buildings Edinburgh EH JZ UK Abstract We develop a formal typ etheoretic account of the basic mechanisms of ob jectoriented programming encapsulatio n message passing subtyping and inheritance By mo deling ob ject encapsulation in terms of existential typ es instead of the recursive records used in other recent studies we obtain a substantial simplicatio n b oth in the mo del of ob jects and in the underlying typ ed calculus Intro duction Static typ e systems for ob jectoriented programming languages have progressed signicantly in the past decade The line of research b egun by Cardelli a Co ok Reddy and Kamin and further develop ed by Car delli Cardelli Wegner Cardelli Mitchell Cardelli a Car delli Mitchell Bruce Wand and many others Canning et al Co ok et al Castagna et al Castagna Ghelli Graver Johnson has culminated in typ etheoretic accounts Bruce Cardelli a Mitchell et al of many of the features of languages like Smalltalk Goldb erg Robson Our goal is to reformulate the essential ideas of these accounts using a simpler typ e theory The key step in our approach is an alternative trea