Institut
de Mathématiques de Luminy
Abstract 2006-07 |
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 |