Bounding normalization time through intersection types

Abstract

Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.

In Proceedings ITRS 2012, arXiv:1307.7849

Cited by in corpus (2)

• The Vectorial $\lambda$-Calculus
• Isomorphisms considered as equalities: Projecting functions and enhancing partial application through and implementation of lambda+