1 Search Results for "Amini, Shahin"

Document

DOI: 10.4230/LIPIcs.CSL.2015.582

On Classical PCF, Linear Logic and the MIX Rule

Authors: Shahin Amini and Thomas Erhard

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract

We study a classical version of PCF from a semantical point of view. We define a general notion of model based on categorical models of Linear Logic, in the spirit of earlier work by Girard, Regnier and Laurent. We give a concrete example based on the relational model of Linear Logic, that we present as a non-idempotents intersection type system, and we prove an Adequacy Theorem using ideas introduced by Krivine. Following Danos and Krivine, we also consider an extension of this language with a MIX construction introducing a form of must non-determinism; in this language, a program of type integer can have more than one value (or no value at all, raising an error). We propose a refinement of the relational model of classical PCF in which programs of type integer are single valued; this model rejects the MIX syntactical constructs (and the MIX rule of Linear Logic).

Cite as

Shahin Amini and Thomas Erhard. On Classical PCF, Linear Logic and the MIX Rule. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 582-596, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{amini_et_al:LIPIcs.CSL.2015.582,
  author =	{Amini, Shahin and Erhard, Thomas},
  title =	{{On Classical PCF, Linear Logic and the MIX Rule}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{582--596},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.582},
  URN =		{urn:nbn:de:0030-drops-54402},
  doi =		{10.4230/LIPIcs.CSL.2015.582},
  annote =	{Keywords: lambda-calculus, linear logic, classical logic, denotational semantics}
}

Refine by Author
1 Amini, Shahin
1 Erhard, Thomas

Refine by Classification

Refine by Keyword
1 classical logic
1 denotational semantics
1 lambda-calculus
1 linear logic

Refine by Type
1 document

Refine by Publication Year
1 2015

1 Search Results for "Amini, Shahin"

On Classical PCF, Linear Logic and the MIX Rule

Abstract

Cite as

Thanks for your feedback!

Could not send message