Execution Time of lambda-Terms via Denotational Semantics and Intersection Types

Simple item page
dc.creatorde Carvalho, Daniel
dc.date2009-05-26
dc.date.accessioned2026-07-07T13:18:16Z
dc.date.available2026-07-07T13:18:16Z
dc.descriptionThe multiset based relational model of linear logic induces a semantics of the type free lambda-calculus, which corresponds to a non-idempotent intersection type system, System R. We prove that, in System R, the size of the type 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.
dc.description36 pages
dc.identifierhttps://arxiv.org/abs/0905.4251
dc.identifierhttp://arxiv.org/abs/0905.4251
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/231379
dc.subjectLogic in Computer Science
dc.subjectComputational Complexity
dc.subjectF.3.2
dc.titleExecution Time of lambda-Terms via Denotational Semantics and Intersection Types
dc.typetext

Files

Collections

arXiv