Execution Time of $\lambda$-Terms via Denotational Semantics and Intersection Types
Résumé
The multiset based relational semantics for linear logic induces a semantics for the type free $\lambda$-calculus. This one is built on non-idempotent intersection types. We prove that the size of the derivations and the size of the types are closely related to the execution time of $\lambda$-terms in a particular environment machine, Krivine's machine.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...