Bounded linear types in a resource semiring

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

Authors

External organisations

  • Birmingham University

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.

Details

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
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
CountryFrance
CityGrenoble
Period5/04/1413/04/14