In this chapter we study the normalization properties of λ&. We show that the λ&-calculus is not strongly normalizing and that it is possible to define in it a fix-point combinator of type (T → T)→ T for every well-formed type T. This expressiveness derives from the definition of the subtyping relation for overloaded types. We give a sufficient condition to have strong normalization, and we define two expressive systems that satisfy it. These systems are important since they will be used in Chapter 10 to study the mathematical meaning of overloading and because they are expressive enough to model object-oriented programming. This chapter is based on a joint work with Giorgio Ghelli and Giuseppe Longo.
Unable to display preview. Download preview PDF.