Fulltext

A Semantics for λ: a Calculus with Overloading and Late‐binding

Studer, Thomas

In: Journal of Logic and Computation, 2001, vol. 11, no. 4, p. 527-544

Add to personal list
    Title
    • A Semantics for λ: a Calculus with Overloading and Late‐binding
    Author
    • Studer, Thomas. Institut für Informatik und angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH-3012 Bern, Switzerland. E-mail: tstuder@iam.unibe.ch
    Document Type
    • Postprint
    Language
    • English
    Published in
    • Journal of Logic and Computation, 2001, vol. 11, no. 4, p. 527-544. Oxford University Press
    Other Version
    OAI-PMH Identifier
    • oai:doc.rero.ch:299442
    Summary
    Up to now there was no interpretation available for λ‐calculi featuring overloading and late‐binding, although these are two of the main principles of any object‐oriented programming language. In this paper we provide a new semantics for a stratified version of Castagna's λ{}, a λ‐calculus combining overloading with late‐binding. The model‐construction is carried out in EETJ + (Tot) + (NF‐I), a system of explicit mathematics. We will prove the soundness of our model with respect to subtyping, type‐checking and reductions. Furthermore, we show that our semantics yields a solution to the problem of loss of information in the context of type‐dependent computations