Abstract
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.
Interestingly, according to modern astronomers, space is finite. This is a very comforting thought — particularly for people who can never remember where they have left things.
Woody Allen
Side-effects. (1981)
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1997 Birkhäuser Boston
About this chapter
Cite this chapter
Castagna, G. (1997). Strong Normalization. In: Object-Oriented Programming A Unified Foundation. Progress in Theoretical Computer Science. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-4138-6_6
Download citation
DOI: https://doi.org/10.1007/978-1-4612-4138-6_6
Publisher Name: Birkhäuser Boston
Print ISBN: 978-1-4612-8670-7
Online ISBN: 978-1-4612-4138-6
eBook Packages: Springer Book Archive