Nous proposons un calcul à ressources adapté à Call-By-Push-Value, à l’aide duquel nous définissons un développement de Taylor. On établit que ce développement est cohérent avec les sémantiques opérationelles et dénotationelles de Call-By-Push-Value en nous inspirant d’outils de la Logique Linéaire. L’essentiel de ce travail consiste à donner une contrepartie syntaxique aux morphismes de coalgèbre de la sémantique.
On examine des méthodes récentes visant à étendre les résultats de Ehrhard et Regnier sur le développement de Taylor : les combinaisons linéaires d’approximants d’un λ-terme peuvent être normalisées sans faire apparaître de coefficients infinis. Les méthodes considérées permettent d’étendre ce résultat à des calculs non uniformes; on montre qu’en se concentrant sur des stratégies d’évaluation précises, comme l’Appel-Par-Valeur, l’Appel-Par-Nécessité, PCF, ou des variantes de l’Appel-Par-Pousse-Valeur (le Bang-Calcul en particulier), l’extension des résultats de finitude de Ehrhard et Regnier peuvent s’appliquer ou non, selon la structure du calcul original. En particulier, on introduit un calcul à ressources pour l’Appel-Par-Nécessité, et montrons que le résultat de finitude de son développement de Taylor peut être dérivé de nos considérations sur l’Appel-Par-Valeur. Nous introduisons aussi un calcul à ressources pour une présentation de PCF avec un point fixe explicite, et montrons comment cela interfère avec le résultat de finitude. On examine ensuite le Bang-Calcul de Ehrhard et Guerrieri, qui possède les propriétés de l’Appel-Par-Pousse-Valeur dans une présentation légèrement différente.
Nous étudions l'élimination des coupures parallèle dans les réseaux de preuve connexes de la logique linéaire multiplicative. Nous donnons une borne à la réduction de la taille et à l'évolution de la longueur des chemins d'interrupteurs sous réduction parallèle, et nous montrons que que ce résultat combinatoire s'applique au développement de Taylor des réseaux de MELL: les coefficients restent finis sous réduction de combinaisons linéaires infinies de réseaux à resource, car ces réseaux se comportent essentiellement comme ceux de MLL.
Nous étendons le résultat de notre article CSL, le généralisant à un fragment plus large de la logique linéaire, incluant les affaiblissements et les unités multiplicatives. Cela exige des méthodes spécifiques pour travailler avec les structures non connexes, en particulier à cause de coupures qui peuvent se réduire dans des sous-structures vides.