Abstract:
We provide a translation of Fisher-Honsell-Mitchell's delegation-based object calculus with subtyping into a lambda-calculus with extensible records. The target type system is an extension of the system $F^\omega$ of dependent types with recursion, extensible records and a form of bounded universal quantification. We show that our translation is computationally adequate, that the typing rules of Fisher-Honsell-Mitchell's calculus can be derived in a rather simple and natural way, and that our system enjoys the standard subject reduction property.

[PostScript, .ps.gz]