Linearity and PCF: a Semantic Insight!

Marco Gaboardi, Luca Paolini, Mauro Piccolo

    Research output: Contribution to journalArticlepeer-review


    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 SlPCF(star), that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. SlPCF(star) 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.

    Original languageEnglish
    Pages (from-to)372-384
    Number of pages13
    JournalACM SIGPLAN Notices
    Issue number9
    Publication statusPublished - Sept 2011


    • PCF
    • Linear Logic
    • Denotational Semantics
    • Operational Semantics
    • Design
    • Theory
    • Languages


    Dive into the research topics of 'Linearity and PCF: a Semantic Insight!'. Together they form a unique fingerprint.

    Cite this