Bounded linear types in a resource semiring

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

Standard

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 proceedingConference contribution

Harvard

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

APA

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

Vancouver

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 ). https://doi.org/10.1007/978-3-642-54833-8_18

Author

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

Bibtex

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

}

RIS

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 -