We present a procedure for computing normal forms of terms in Abadi and
Cardelli's functional object calculus. Even when equipped with simple types,
terms of this calculus are not terminating in general, and we draw on recent
ideas about the normalization by evaluation paradigm for the untyped
lambda calculus. Technically, we work in the framework of Shinwell and Pitts'
FM-domain theory, which leads to a normalization procedure for the object
calculus that is directly implementable in a language like Fresh O'Caml.
Download PDF Show BibTeX
Login to edit