Projects per year
Abstract
We investigate the possibility of a semantic account of the execution time (i.e. the number of β_{v}steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin’s callbyvalue λcalculus. For this purpose, we use a linear logic based denotational model that can be seen as a nonidempotent intersection type system: relational semantics. Our investigation is inspired by similar ones for linear logic proofnets and untyped callbyname λcalculus. We first prove a qualitative result: a (possibly open) term is normalizable for weak reduction (which does not reduce under abstractions) if and only if its interpretation is not empty. We then show that the size of type derivations can be used to measure the execution time. Finally, we show that, differently from the case of linear logic and callbyname λcalculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). To get a truly semantic measure of execution time in a callbyvalue setting, we conjecture that a refinement of its syntax and operational semantics is needed.
Original language  English 

Pages (fromto)  5772 
Number of pages  16 
Journal  Electronic Proceedings in Theoretical Computer Science, EPTCS 
Volume  293 
DOIs  
Publication status  Published  2019 
Event  12th Workshop on Developments in Computational Models, DCM 2018 and 9th Workshop on Intersection Types and Related Systems, ITRS 2018  Oxford, UK United Kingdom Duration: 8 Jul 2018 → 8 Jul 2018 
ASJC Scopus subject areas
 Software
Fingerprint Dive into the research topics of 'Towards a semantic measure of the execution time in callbyvalue lambdacalculus'. Together they form a unique fingerprint.
Projects
 1 Active

Typed LambdaCalculi with Sharing and Unsharing
Engineering and Physical Sciences Research Council
1/01/19 → 31/12/21
Project: Research council