Abstract
A polarized version of Girard, Scedrov and Scott’s Bounded Linear Logic is introduced and its normalization properties studied. Following Laurent [25], the logic naturally gives rise to a type system for the λμ-calculus, whose derivations reveal bounds on the time complexity of the underlying term. This is the first example of a type system for the λμ-calculus guaranteeing time complexity bounds for typable programs.
An extended version of this paper including more details is available [9].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Accattoli, B., Dal Lago, U.: On the invariance of the unitary cost model for head reduction. In: RTA. LIPIcs, vol. 15, pp. 22–37 (2012)
Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 871–885. Springer, Heidelberg (2003)
Baillot, P., Coppola, P., Dal Lago, U.: Light logics and optimal reduction: Completeness and complexity. Information and Computation 209(2), 118–142 (2011)
Baillot, P., Mazza, D.: Linear logic by levels and bounded time complexity. Theoretical Computer Science 411(2), 470–503 (2010)
Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. Information and Computation 207(1), 41–62 (2009)
Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP, pp. 233–243. ACM (2000)
Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. Logical Methods in Computer Science 8(4) (2012)
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)
Dal Lago, U., Pellitta, G.: Complexity analysis in presence of control operators and higher-order functions (long version), http://arxiv.org/abs/1310.1763
de Bakker, J.W., de Bruin, A., Zucker, J.: Mathematical theory of program correctness. Prentice-Hall International Series in Computer Science. Prentice Hall (1980)
de Groote, P.: A CPS-translation of the λμ-calculus. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 85–99. Springer, Heidelberg (1994)
de Groote, P.: On the relation between the λμ-calculus and the syntactic theory of sequential control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 31–43. Springer, Heidelberg (1994)
de Groote, P.: An environment machine for the λμ-calculus. Mathematical Structures in Computer Science 8(6), 637–669 (1998)
Felleisen, M.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP 1990. LNCS, vol. 432, pp. 134–151. Springer, Heidelberg (1990)
Gaboardi, M., Ronchi Della Rocca, S.: A soft type assignment system for lambda-calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 253–267. Springer, Heidelberg (2007)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50(1), 1–101 (1987)
Girard, J.-Y.: A new constructive logic: Classical logic. Mathematical Structures in Computer Science 1(3), 255–296 (1991)
Girard, J.-Y.: Light linear logic. Information and Computation 143(2), 175–204 (1998)
Girard, J.-Y., Scedrov, A., Scott, P.: Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science 97(1), 1–66 (1992)
Griffin, T.: A formulae-as-types notion of control. In: POPL, pp. 47–58. ACM Press (1990)
Gulwani, S.: Speed: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 51–62. Springer, Heidelberg (2009)
Jost, S., Hammond, K., Loidl, H.-W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: POPL, Madrid, Spain. ACM Press (2010)
Lafont, Y.: Soft linear logic and polynomial time. Theoretical Computer Science 318(1), 163–180 (2004)
Laurent, O.: Étude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (March 2002)
Laurent, O.: Polarized proof-nets and λμ-calculus. Theoretical Computer Science 290(1), 161–188 (2003)
Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: POPL, pp. 215–227. ACM Press (1997)
Parigot, M.: λμ-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS (LNAI), vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Schöpp, U.: Stratified bounded affine logic for logarithmic space. In: LICS, pp. 411–420 (2007)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenström, P.: The worst case execution time problem - overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dal Lago, U., Pellitta, G. (2013). Complexity Analysis in Presence of Control Operators and Higher-Order Functions. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)