| Compositional Characterisations of λ-terms using Intersection Types (2005) | |||||||||||||||||
Abstract | |||||||||||||||||
| We show how to characterise compositionally a number of evaluation properties of #-terms using Intersection Type assignment systems. In particular, we focus on termination properties, such as strong normalisation, normalisation, head normalisation, and weak head normalisation. We consider also the persistent versions of such notions. By way of example, we consider also another evaluation property, unrelated to termination, namely reducibility to a closed term. | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||