An Interpretation of Extensible Objects

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ω 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.

Publication
In FCT’9912th International Symposium on Fundamentals of Computation Theory