eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2011-08-31
97
111
10.4230/LIPIcs.CSL.2011.97
article
Full Abstraction for Resource Calculus with Tests
Bucciarelli, Antonio
Carraro, Alberto
Ehrhard, Thomas
Manzonetto, Giulio
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol012-csl2011/LIPIcs.CSL.2011.97/LIPIcs.CSL.2011.97.pdf
resource lambda calculus
relational semantics
full abstraction
differential linear logic