Bounded linear types in a resource semiring

Dan R. Ghica; Alex I. Smith

doi:10.1007/978-3-642-54833-8_18

Bounded linear types in a resource semiring

Dan R. Ghica, Alex I. Smith

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

22 Citations (Scopus)

237 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 language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	23rd 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
Publisher	Springer
Pages	331-350
Number of pages	20
Volume	8410
ISBN (Print)	9783642548321
DOIs	https://doi.org/10.1007/978-3-642-54833-8_18
Publication status	Published - 2014
Event	23rd 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 2014 → 13 Apr 2014

Publication series

Name	Lecture Notes in Computer Science
Volume	8410
ISSN (Print)	0302-9743
ISSN (Electronic)	16113349

Conference

Conference	23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Country/Territory	France
City	Grenoble
Period	5/04/14 → 13/04/14

ASJC Scopus subject areas

Computer Science(all)
Theoretical Computer Science

Access to Document

10.1007/978-3-642-54833-8_18Licence: None: All rights reserved

Ghica_&_Smith_Bounded_linear_types_Programming_languages_and_systems_2014Accepted author manuscript, 381 KBLicence: None: All rights reserved

A Higher Order approach to Codesign
Ghica, D.
Engineering & Physical Science Research Council
17/06/13 → 16/12/16
Project: Research Councils

Cite this

Ghica, D. R., & Smith, A. I. (2014). Bounded linear types in a resource semiring. In Programming Languages and Systems: 23rd 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 (Vol. 8410, pp. 331-350). (Lecture Notes in Computer Science ; Vol. 8410). Springer. https://doi.org/10.1007/978-3-642-54833-8_18

Ghica, Dan R. ; Smith, Alex I. / Bounded linear types in a resource semiring. Programming Languages and Systems: 23rd 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. Vol. 8410 Springer, 2014. pp. 331-350 (Lecture Notes in Computer Science ).

@inproceedings{880a8624b9dd4a54a16eec5173d3e315,

title = "Bounded linear types in a resource semiring",

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.",

author = "Ghica, {Dan R.} and Smith, {Alex I.}",

year = "2014",

doi = "10.1007/978-3-642-54833-8_18",

language = "English",

isbn = "9783642548321",

volume = "8410",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "331--350",

booktitle = "Programming Languages and Systems",

note = "23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 ; Conference date: 05-04-2014 Through 13-04-2014",

}

Ghica, DR & Smith, AI 2014, Bounded linear types in a resource semiring. in Programming Languages and Systems: 23rd 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. vol. 8410, Lecture Notes in Computer Science , vol. 8410, Springer, pp. 331-350, 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, 5/04/14. https://doi.org/10.1007/978-3-642-54833-8_18

Bounded linear types in a resource semiring. / Ghica, Dan R.; Smith, Alex I.
Programming Languages and Systems: 23rd 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. Vol. 8410 Springer, 2014. p. 331-350 (Lecture Notes in Computer Science ; Vol. 8410).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Bounded linear types in a resource semiring

AU - Ghica, Dan R.

AU - Smith, Alex I.

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84900522404&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-54833-8_18

DO - 10.1007/978-3-642-54833-8_18

M3 - Conference contribution

AN - SCOPUS:84900522404

SN - 9783642548321

VL - 8410

T3 - Lecture Notes in Computer Science

SP - 331

EP - 350

BT - Programming Languages and Systems

PB - Springer

T2 - 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014

Y2 - 5 April 2014 through 13 April 2014

ER -

Ghica DR, Smith AI. Bounded linear types in a resource semiring. In Programming Languages and Systems: 23rd 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. Vol. 8410. Springer. 2014. p. 331-350. (Lecture Notes in Computer Science ). doi: 10.1007/978-3-642-54833-8_18

Bounded linear types in a resource semiring

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Fingerprint

Projects

A Higher Order approach to Codesign

Cite this