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

 


Last update : may 4, 2006, EL.