2026-08-06T12:18:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11659 2024-03-06T10:48:43Z ddc:004 open_access

Taylor expansion for Call-By-Push-Value Chouquet, Jules Tasson, Christine Call-By-Push-Value Quantitative semantics Taylor expansion Linear Logic The connection between the Call-By-Push-Value lambda-calculus introduced by Levy and Linear Logic introduced by Girard has been widely explored through a denotational view reflecting the precise ruling of resources in this language. We take a further step in this direction and apply Taylor expansion introduced by Ehrhard and Regnier. We define a resource lambda-calculus in whose terms can be used to approximate terms of Call-By-Push-Value. We show that this approximation is coherent with reduction and with the translations of Call-By-Name and Call-By-Value strategies into Call-By-Push-Value. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jules Chouquet and Christine Tasson 2020 Is Part Of LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2020.16 urn:nbn:de:0030-drops-116594 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.16 eng https://creativecommons.org/licenses/by/3.0/legalcode