Full Abstraction for Resource Calculus with Tests

Bucciarelli, Antonio; Carraro, Alberto; Ehrhard, Thomas; Manzonetto, Giulio

doi:10.4230/LIPIcs.CSL.2011.97

Document

Full Abstraction for Resource Calculus with Tests

Authors Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, Giulio Manzonetto

Part of: Volume: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (CSL 2011)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Computer Science Logic (CSL)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2011-08-31

PDF

File

PDF

LIPIcs.CSL.2011.97.pdf

Filesize: 0.56 MB
15 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CSL.2011.97
URN: urn:nbn:de:0030-drops-32250

Subject Classification

Keywords

resource lambda calculus
relational semantics
full abstraction
differential linear logic

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get BibTex

Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full Abstraction for Resource Calculus with Tests. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 97-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011) https://doi.org/10.4230/LIPIcs.CSL.2011.97

Author Details

Antonio Bucciarelli

Alberto Carraro

Thomas Ehrhard

Giulio Manzonetto

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail