Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

paolini11icfp (In proceedings)
Author(s) Marco Gaboardi, Luca Paolini and Mauro Piccolo
Title« Linearity and PCF: a semantic insight! »
InICFP 2011 - The 16th ACM SIGPLAN International Conference on Functional Programming
Page(s)372-384
Year2011
PublisherACM, USA
Abstract
Linearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces. We introduce a language, named StPCF, that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. StPCF allows us to program all the finite elements of the model and, consequently, it entails a full abstraction result that makes the reasoning on the equivalence between programs simpler. Denotational linearity provides also crucial information for the operational evaluation of programs. We formalize two evaluation machineries for the language. The first one is an abstract and concise operational semantics designed with the aim of explaining the new operators, and is based on an infinite-branching search of the evaluation space. The second one is more concrete and it prunes such a space, by exploiting the linear assumptions. This can also be regarded as a base for an implementation.

Download the complete article: Linearity and PCF: a semantic insight - ICFP 2012.pdf

BibTeX code

@inproceedings{paolini11icfp,
  author = {Gaboardi, Marco and Paolini, Luca and Piccolo, Mauro},
  booktitle = {ICFP 2011 - The 16th ACM SIGPLAN International Conference on
               Functional Programming },
  abstract = { Linearity is a multi-faceted and ubiquitous notion in the
              analysis and the development of programming language concepts. We
              study linearity in a denotational perspective by picking out
              programs that correspond to linear functions between coherence
              spaces. We introduce a language, named StPCF, that increases the
              higher-order expressivity of a linear core of PCF by means of new
              operators related to exception handling and parallel evaluation.
              StPCF allows us to program all the finite elements of the model
              and, consequently, it entails a full abstraction result that makes
              the reasoning on the equivalence between programs simpler.
              Denotational linearity provides also crucial information for the
              operational evaluation of programs. We formalize two evaluation
              machineries for the language. The first one is an abstract and
              concise operational semantics designed with the aim of explaining
              the new operators, and is based on an infinite-branching search of
              the evaluation space. The second one is more concrete and it
              prunes such a space, by exploiting the linear assumptions. This
              can also be regarded as a base for an implementation.},
  title = {Linearity and {PCF}: a semantic insight!},
  tag = {ICFP 2011},
  localfile = {http://www.di.unito.it/~paolini/papers/Linearity and PCF: a semantic insight - ICFP 2012.pdf},
  publisher = {ACM, USA},
  pages = {372-384},
  year = 2011,
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!