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