Logo - springer
Slogan - springer

Birkhäuser - Birkhäuser Computer Science | Object-Oriented Programming A Unified Foundation

Object-Oriented Programming A Unified Foundation

Castagna, Giuseppe

1997, XVIII, 366 p.

A product of Birkhäuser Basel
Available Formats:

Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.

You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.

After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.


(net) price for USA

ISBN 978-1-4612-4138-6

digitally watermarked, no DRM

Included Format: PDF

download immediately after purchase

learn more about Springer eBooks

add to marked items


Hardcover version

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-0-8176-3905-1

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days

add to marked items


Softcover (also known as softback) version.

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-1-4612-8670-7

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days

add to marked items

  • About this book

by Luea Cardelli Ever since Strachey's work in the 1960's, polymorphism has been classified into the parametric and overloading varieties. Parametric polymorphism has been the subject of extensive study for over two decades. Overloading, on the other hand, has often been considered too ad hoc to deserve much attention even though it has been, in some form, an ingredient of virtually every programming lan­ guage (much more so than parametric polymorphism). With the introduction of object-oriented languages, and in particular with multiple-dispatch object-oriented languages, overloading has become less of a programming convenience and more of a fundamental feature in need of proper explanation. This book provides a compelling framework for the study of run-time over­ loading and of its interactions with subtyping and with parametric polymorphism. The book also describes applications to object-oriented programming. This new framework is motivated by the relatively recent spread of programming languages that are entirely based on run-time overloading; this fact probably explains why this subject was not investigated earlier. Once properly understood, overloading reveals itself relevant also to the study of older and more conventional (single­ dispatch) object-oriented languages, clarifying delicate issues of covariance and contravariance of method types, and of run-time type analysis. In the final chapters, a synthesis is made between parametric and overloading polymorphism.

Content Level » Research

Keywords » Inform - algorithms - class - object - object-oriented programming - overloading - polymorphism - programming

Related subjects » Birkhäuser Computer Science

Table of contents 

I Introduction.- 1 Background and notation.- 1.1 ?-notation.- 1.1.1 The origins of ?-calculus.- 1.1.2 Datatypes.- 1.2 Simply-typed ?-calculus.- 1.2.1 Reduction.- 1.2.2 Typing.- 1.2.3 Properties.- 1.2.4 Fixed point operators.- 1.3 Subtyping.- 1.3.1 The ??-calculus.- 1.3.2 Records.- 1.3.3 Cartesian products.- 1.3.4 Recursive types.- 1.4 Further definitions.- 1.4.1 Algebra.- 1.4.2 Term rewriting systems.- 1.4.3 Logic.- 2 A quick overview.- 2.1 Introduction.- 2.2 Object-oriented programming.- 2.3 The ?&-calculus.- 2.4 Covariance and contravariance.- 2.5 Strong normalization.- 2.6 Three variations on the theme.- 2.7 Interpretation of object-oriented languages.- 2.8 Imperative features.- 2.9 Semantics.- 2.10 Second-order.- 2.11 Second order overloading.- 2.12 F?& and object-oriented programming.- 2.13 Conclusion.- II Simple typing.- 3 Object-oriented programming.- 3.1 A kernel object-oriented language.- 3.1.1 Objects.- 3.1.2 Messages.- 3.1.3 Methods versus functions.- 3.1.4 Classes.- 3.1.5 Inheritance.- 3.1.6 Multiple inheritance.- 3.1.7 Implementation of message-passing.- 3.1.8 Extending classes.- 3.1.9 Self, super and the use of coercions.- 3.1.10 First-class messages: adding overloading.- 3.1.11 Multi-methods.- 3.2 Type checking.- 3.2.1 The types.- 3.2.2 Intuitive typing rules.- 3.3 Object-oriented programming à la CLOS.- 3.3.1 Classes.- 3.3.2 Methods.- 3.3.3 Multiple dispatching.- 3.3.4 Super and coerce.- 3.3.5 Types.- 3.4 Comparison.- 3.5 Conclusion.- 3.6 Bibliographical notes.- 4 The ?&-calculus.- 4.1 Informal presentation.- 4.1.1 Subtyping, run-time types and late binding.- 4.2 The syntax of ?&-calculus.- 4.2.1 Subtyping system.- 4.2.2 Types.- 4.2.3 Terms.- 4.2.4 Type system.- 4.2.5 Reduction Rules.- 4.3 Soundness of the type system.- 4.4 Church-Rosser.- 4.5 Basic encodings.- 4.5.1 Products.- 4.5.2 Simple records.- 4.5.3 Updatable records.- 4.6 ?& and object-oriented programming.- 4.6.1 The “objects as records” analogy.- 4.6.2 Inheritance.- 4.6.3 Binary methods and multiple dispatch.- 4.6.4 Covariance vs. contravariance.- 4.6.5 Class extension.- 4.6.6 First class messages.- 4.6.7 Abstract classes.- 4.7 Related work.- 5 Covariance and contravariance: conflict without a cause.- 5.1 Introduction.- 5.2 The controversy.- 5.3 Covariance in the overloading-based model.- 5.4 Covariance in the record-based model.- 5.5 Practical aspects.- 5.6 Conclusion.- 6 Strong Normalization.- 6.1 The full calculus is not normalizing.- 6.2 Fixed point combinators.- 6.3 The reasons for non normalization.- 6.4 Typed-inductive properties.- 6.5 Strong Normalization is typed-inductive.- 7 Three variations on the theme.- 7.1 Adding explicit coercions.- 7.1.1 Properties.- 7.1.2 More on updatable records.- 7.2 More freedom to the system: ?&+.- 7.3 Unifying overloading and ?-abstraction: ?{}.- 7.3.1 Subject Reduction.- 7.3.2 Church-Rosser.- 7.4 Reference to other work.- 8 Interpretation of object-oriented languages.- 8.1 Formal presentation of KOOL.- 8.1.1 The terms of the language.- 8.1.2 The types of the language.- 8.2 ?_object.- 8.2.1 The type system.- 8.2.2 Some results.- 8.3 Translation.- 8.3.1 Correctness of the type-checking.- 8.3.2 Some remarks.- 8.4 ?_object and ?&.- 8.4.1 The encoding of the types.- 8.4.2 The encoding of the terms.- 9 Imperative features and other widgets.- 9.1 Imperative features.- 9.1.1 Imperative KOOL.- 9.1.2 Imperative ?&-calculus.- 9.1.3 Interpretation.- 9.2 Unique application.- 9.3 Signatures.- 10 Semansttics.- 10.1 Introduction.- 10.2 The completion of overloaded types.- 10.3 Early Binding.- 10.4 Semantics.- 10.4.1 PER as a model.- 10.4.2 Overloaded types as Products.- 10.4.3 The semantics of terms.- 10.5 Summary of the semantics.- III Second order.- 11 Introduction to part III.- 11.1 Loss of information in the record-based model.- 11.1.1 Implicit Polymorphism.- 11.1.2 Explicit Polymorphism.- 11.2 F?.- 11.2.1 Subtyping and typing algorithms.- 11.3 Further features.- 11.3.1 Records and update.- 11.3.2 Quantification over recursive types.- 11.3.3 F-bounded quantification.- 11.3.4 Existential quantification.- 12 Second order overloading.- 12.1 Loss of information in the overloading-based model.- 12.1.1 Type dependency.- 12.2 Type system.- 12.2.1 Some useful results.- 12.2.2 Transitivity elimination.- 12.2.3 Subtyping algorithm and coherence of the system.- 12.3 Terms.- 12.4 Reduction.- 12.4.1 Soundness of the type system.- 12.4.2 Church-Rosser.- 13 Second order overloading and object-oriented programming.- 13.1 Object-oriented programming.- 13.1.1 Extending classes.- 13.1.2 First class messages, super and coerce.- 13.1.3 Typing rules for polymorphic KOOL.- 13.1.4 Multiple dispatch.- 13.1.5 Advanced features.- 13.2 Conclusion.- 14 Conclusion.- 14.1 Object-oriented programming.- 14.2 Proof Theory.- 14.3 Beyond object-oriented programming.- IV Appendixes.- A Specification of KOOL.- A.1 Terms.- A.2 Pretypes.- A.3 Subtyping.- A.4 Auxiliary Notation.- A.5 Typing Rules.- B Formal definition of the translation.- B.1 Without mutually recursive methods.- B.2 With recursive methods.- B.3 Overloaded functions.- B.4 Correctness of the type-checking.

Popular Content within this publication 



Read this Book on Springerlink

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Programming Techniques.

Additional information