Strong Normalization

  • Giuseppe Castagna
Part of the Progress in Theoretical Computer Science book series (PTCS)


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 (TT)→ 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.


Strong Normalization Closed Term Primed Term Subtyping Relation Subject Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Birkhäuser Boston 1997

Authors and Affiliations

  • Giuseppe Castagna
    • 1
  1. 1.CNRS, LIENSParisFrance

Personalised recommendations