Daniel de Carvalho

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

2017 · Mathematical Structures in Computer Science

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 …