Execution time of λ-terms via denotational semantics and intersection types

The multiset-based relational model of linear logic induces a semantics of the untyped λ-calculus, which corresponds with a non-idempotent intersection type system, System R . We prove that, in System R , the size of type derivations and the size of types are closely related to the execution time of λ-terms in a particular environment machine, Krivine's machine.