Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 11, Issue 4, pp. 527-544: Abstract.

A Semantics for [lambda]: a Calculus with Overloading and Late-binding

Thomas Studer

Institut für Informatik und angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH-3012 Bern, Switzerland. E-mail: tstuder@iam.unibe.ch

Up to now there was no interpretation available for [lambda]-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 [lambda]{}, a [lambda]-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.

Keywords: Explicit mathematics, typed [lambda], -, calculus, overloading, late-, binding, loss of information

  Full-Text PDF  (236 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.