Execution Time of lambda-Terms via Denotational Semantics and Intersection Types

Daniel de Carvalho

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.…