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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Boudol, G.: The lambda-calculus with multiplicities (abstract). In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 1–6. Springer, Heidelberg (1993)
Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 351–370. Springer, Heidelberg (2014)
Crary, K., Weirich, S.: Resource bound certification. In: POPL 2000, pp. 184–198. ACM, New York (2000)
Lago, U.D., Gaboardi, M.: Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8(4) (2011)
Dal Lago, U., Hofmann, M.: Bounded linear logic, revisited. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 80–94. Springer, Heidelberg (2009)
Lago, U.D., Petit, B.: The geometry of types. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 167–178. ACM (2013)
Dan, R.: Ghica. Slot games: a quantitative model of computation. In: POPL 2005, Long Beach, California, USA, January 12-14, pp. 85–97. ACM (2005)
Dan, R.: Ghica. Geometry of Synthesis: a structured approach to VLSI design. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 363–375. ACM (2007)
Ghica, D.R., Murawski, A.S.: Compositional model extraction for higher-order concurrent programs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 303–317. Springer, Heidelberg (2006)
Ghica, D.R., Murawski, A.S., Luke Ong, C.-H.: Syntactic control of concurrency. Theor. Comput. Sci. 350(2-3), 234–251 (2006)
Ghica, D.R., Smith, A.: Geometry of synthesis iii: resource management through type inference. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 345–356. ACM (2011)
Ghica, D.R., Smith, A.: From bounded affine types to automatic timing analysis. CoRR, abs/1307.2473 (2013)
Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science 97(1), 1–66 (1992)
Hofmann, M.: Linear types and non-size-increasing polynomial time computation. In: LICS, pp. 464–473. IEEE Computer Society (1999)
Kelly, G.M.: On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra 1(4), 397–402 (1964)
Laird, J., Manzonetto, G., McCusker, G., Pagani, M.: Weighted relational models of typed lambda-calculi. In: LICS, pp. 301–310. IEEE Computer Society (2013)
Melliès, P.-A., Tabareau, N.: An algebraic account of references in game semantics. Electr. Notes Theor. Comput. Sci. 249, 377–405 (2009)
Melliès, P.-A., Tabareau, N.: Resource modalities in tensor logic. Ann. Pure Appl. Logic 161(5), 632–653 (2010)
Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17(3), 348–375 (1978)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
O’Hearn, P.W.: On bunched typing. J. Funct. Program. 13(4), 747–796 (2003)
Reynolds, J.C.: The essence of ALGOL. In: ALGOL-like Languages, vol. 1, pp. 67–88. Birkhauser Boston Inc. (1997)
John, C.: Reynolds. Syntactic control of interference. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) POPL, pp. 39–46. ACM Press (1978)
Smith, A.: Type-directed hardware synthesis. PhD thesis, University of Birmingham (forthcoming)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ghica, D.R., Smith, A.I. (2014). Bounded Linear Types in a Resource Semiring. In: Shao, Z. (eds) Programming Languages and Systems. ESOP 2014. Lecture Notes in Computer Science, vol 8410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54833-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-54833-8_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54832-1
Online ISBN: 978-3-642-54833-8
eBook Packages: Computer ScienceComputer Science (R0)