de Mathématiques de Luminy
de Carvalho Daniel.
Execution time of lambda-terms via non uniform semantics and intersection types
The relational semantics for Linear Logic induces a semantics for the type free Lambda Calculus. This one is built on non-idempotent intersection types. We give a principal typing property for this type system. We then prove that the size of the derivations is closely related to the execution time of lambda-terms in a particular environment machine, Krivine’s machine.
Keywords. abstract machines, denotational semantics, intersection types, lambda-calculus, linear logic