Inheritance and explicit coercion

V. Breazu-Tannen, T. Coquand, Carl Gunter, A. Scedrov

Research output: Chapter in Book/Report/Conference proceedingConference contribution


A method is presented for providing semantic interpretations for languages which feature inheritance in the framework of statically checked, rich type disciplines. The approach is illustrated by an extension of the language Fun of L. Cardelli and P. Wegner (1985), which is interpreted via a translation into an extended polymorphic lambda calculus. The approach interprets inheritances in Fun as coercion functions already definable in the target of the translation. Existing techniques in the theory of semantic domains can then be used to interpret the extended polymorphic lambda calculus, thus providing many models for the original language. The method allows the simultaneous modeling of parametric polymorphism, recursive types, and inheritance, which has been regarded as problematic because of the seemingly contradictory characteristics of inheritance and type recursion on higher types. The main difficulty in providing interpretations for explicit type disciplines featuring inheritance, namely, that programs can type-check in more than one way, is identified. Since interpretations follow the type-checking derivations, coherence theorems are required (that is, one must prove that the meaning of a program does not depend on the way it was type-checked), and the authors prove them for their semantic method.

Original languageEnglish (US)
Title of host publicationProc Fourth Ann Symp Logic Comput Sci
Editors Anon
PublisherPubl by IEEE
Number of pages18
ISBN (Print)0818619546
StatePublished - 1989
Externally publishedYes
EventProceedings of the Fourth Annual Symposium on Logic in Computer Science - Pacific Grove, CA, USA
Duration: Jun 5 1989Jun 8 1989


OtherProceedings of the Fourth Annual Symposium on Logic in Computer Science
CityPacific Grove, CA, USA

ASJC Scopus subject areas

  • Engineering(all)


Dive into the research topics of 'Inheritance and explicit coercion'. Together they form a unique fingerprint.

Cite this