Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.97
URN: urn:nbn:de:0030-drops-32250
URL: https://drops.dagstuhl.de/opus/volltexte/2011/3225/
Bucciarelli, Antonio ; Carraro, Alberto ; Ehrhard, Thomas ; Manzonetto, Giulio
Full Abstraction for Resource Calculus with Tests
| pdf-format: |
|
Abstract
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.
BibTeX - Entry
@InProceedings{bucciarelli_et_al:LIPIcs:2011:3225,
author = {Antonio Bucciarelli and Alberto Carraro and Thomas Ehrhard and Giulio Manzonetto},
title = {{Full Abstraction for Resource Calculus with Tests}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {97--111},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Marc Bezem},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3225},
URN = {urn:nbn:de:0030-drops-32250},
doi = {10.4230/LIPIcs.CSL.2011.97},
annote = {Keywords: resource lambda calculus, relational semantics, full abstraction, differential linear logic}
}
| Keywords: | resource lambda calculus, relational semantics, full abstraction, differential linear logic | |
| Seminar: | Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL | |
| Issue date: | 2011 | |
| Date of publication: | 31.08.2011 |
