IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fourth Annual IEEE Symposium on

Logic in Computer Science (LICS 1989)

Paper: Inheritance and explicit coercion (at LICS 1989)

Authors: Val Breazu-Tannen Thierry Coquand Carl A. Gunter Andre Scedrov


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 is identified. Since interpretations follow the type-checking derivations, coherence theorems are required, and the authors prove them for their semantic method


    author = 	 {Val Breazu-Tannen and Thierry Coquand and Carl A. Gunter and Andre Scedrov},
    title = 	 {Inheritance and explicit coercion},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)},
    year =	 {1989},
    month =	 {June}, 
    pages =      {112--129},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2018-06-2121:59
Andrzej Murawski