Bounded linear types in a resource semiring

Dan R. Ghica, Alex I. Smith

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    22 Citations (Scopus)
    143 Downloads (Pure)

    Abstract

    Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce a bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a (coherent) categorical semantics. This could be a useful type-theoretic and denotational framework for resource-sensitive compilation, and it represents a generalization of several existing type systems. As a non-trivial instance, motivated by hardware compilation, we present a complex new application to calculating and controlling timing of execution in a (recursion-free) higher-order functional programming language with local store.

    Original languageEnglish
    Title of host publicationProgramming Languages and Systems
    Subtitle of host publication23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings
    PublisherSpringer
    Pages331-350
    Number of pages20
    Volume8410
    ISBN (Print)9783642548321
    DOIs
    Publication statusPublished - 2014
    Event23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - Grenoble, France
    Duration: 5 Apr 201413 Apr 2014

    Publication series

    NameLecture Notes in Computer Science
    Volume8410
    ISSN (Print)0302-9743
    ISSN (Electronic)16113349

    Conference

    Conference23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
    Country/TerritoryFrance
    CityGrenoble
    Period5/04/1413/04/14

    ASJC Scopus subject areas

    • Computer Science(all)
    • Theoretical Computer Science

    Fingerprint

    Dive into the research topics of 'Bounded linear types in a resource semiring'. Together they form a unique fingerprint.

    Cite this