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).
@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.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} }
Feedback for Dagstuhl Publishing