Type Assigment Systems for Lambda Calculi and for the Lambda Calculus of Objects

Data Types and Existential-Types : : : : : : : : : : : : : : : : 108 5.2.1 The Existential Model of Pierce and Turner : : : : : : : : : : : : 110 5.2.2 Methods and Object-Types : : : : : : : : : : : : : : : : : : : : : 111 5.2.3 Methods and Objects : : : : : : : : : : : : : : : : : : : : : : : : : 112 5.2.4 Methods and Message Send : : : : : : : : : : : : : : : : : : : : : 112 5.2.5 Classes and Inheritance : : : : : : : : : : : : : : : : : : : : : : : : 113 5.2.6 Conclusions : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 115 5.3 The Primitive Object Calculus of Abadi and Cardelli : : : : : : : : : : : 116 5.3.1 Syntax and Operational Semantics : : : : : : : : : : : : : : : : : 117 5.3.2 The Type System: a Survey : : : : : : : : : : : : : : : : : : : : : 119 5.3.3 Adding Subtyping : : : : : : : : : : : : : : : : : : : : : : : : : : : 121 5.3.4 Adding Recursive-Types : : : : : : : : : : : : : : : : : : : : : : : 122 CONTENTS 3 6 The Lambda Calculus of Objects 125 6.1 The obj : Syntax and Semantics : : : : : : : : : : : : : : : : : : : : : : : 126 6.1.1 Syntax of the Core Language : : : : : : : : : : : : : : : : : : : : 126 6.1.2 The Operational Semantics of obj : : : : : : : : : : : : : : : : : 127 6.1.3 Examples of Objects, Inheritance and Self-References : : : : : : : 129 6.2 Static Type System : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 131 6.2.1 Static and Strong Typing : : : : : : : : : : : : : : : : : : : : : : 131 6.2.2 Message-Send and Method Specialization : : : : : : : : : : : : : : 131 6.2.3 Operational Equivalence and Objects-Types : : : : : : : : : : : : 132 6.2.4 Syntax of the Type System : : : : : : : : : : : : : : : : : : : : : 133 6.2.5 Analysis of the Main Typing Rules : : : : : : : : : : : : : : : : : 134 6.2.6 Example of ...