2026-07-20T10:41:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3225 2024-03-06T10:33:58Z ddc:004 open_access

Full Abstraction for Resource Calculus with Tests Bucciarelli, Antonio Carraro, Alberto Ehrhard, Thomas Manzonetto, Giulio resource lambda calculus relational semantics full abstraction differential linear logic We study the semantics of a resource sensitive extension of the lambda-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D infinity model of the pure lambda-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a ``must'' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Antonio Bucciarelli and Alberto Carraro and Thomas Ehrhard and Giulio Manzonetto 2011 Is Part Of LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2011.97 urn:nbn:de:0030-drops-32250 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.97 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode