Infinitary Intersection Types as Sequences: a New Answer to Klop's Question

Pierre Vial

We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempoten…