skip to main content
10.1145/2429069.2429090acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

The geometry of types

Published: 23 January 2013 Publication History

Abstract

We show that time complexity analysis of higher-order functional programs can be effectively reduced to an arguably simpler (although computationally equivalent) verification problem, namely checking first-order inequalities for validity. This is done by giving an efficient inference algorithm for linear dependent types which, given a PCF term, produces in output both a linear dependent type and a cost expression for the term, together with a set of proof obligations. Actually, the output type judgement is derivable iff all proof obligations are valid. This, coupled with the already known relative completeness of linear dependent types, ensures that no information is lost, i.e., that there are no false positives or negatives. Moreover, the procedure reflects the difficulty of the original problem: simple PCF terms give rise to sets of proof obligations which are easy to solve. The latter can then be put in a format suitable for automatic or semi-automatic verification by external solvers. Ongoing experimental evaluation has produced encouraging results, which are briefly presented in the paper.

Supplementary Material

JPG File (r1d1_talk11.jpg)
MP4 File (r1d1_talk11.mp4)

References

[1]
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. I & C 163(2), 409--470 (2000)
[2]
Amadio, R.M., Regis-Gianas, Y.: Certifying and reasoning on cost annotations of functional programs. CoRR abs/1110.2350 (2011)
[3]
de Bakker, J.W.: Mathematical Theory of Program Correctness. Prentice-Hall (1980)
[4]
Barthe, G., Grégoire, B., Riba, C.: Type-based termination with sized products. In: CSL 2008. LNCS, vol. 5213, pp. 493--507. Springer (2008)
[5]
Benzinger, R.: Automated higher-order complexity analysis. Theor. Comput. Sci. 318(1-2), 79--103 (2004)
[6]
Bobot, F., Filliatre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: First InternationalWorkshop on Intermediate Verification Languages. pp. 53--64 (2011)
[7]
Clarke, E.M.: Programming language constructs for which it is impossible to obtain good hoare axiom systems. J. ACM 26(1), 129--147 (1979)
[8]
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: RTA 2003. LNCS, vol. 2706, pp. 76--87 (2003)
[9]
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. on Computing 7, 70--90 (1978)
[10]
Dal Lago, U.: Context semantics, linear logic and computational complexity. In: LICS 2006. pp. 169--178 (2006)
[11]
Dal Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: LICS 2011. pp. 133--142 (2011)
[12]
Dal Lago, U., Petit, B.: The geometry of types (long version) (2012), available at http://arxiv.org/abs/1210.6857
[13]
Dal Lago, U., Petit, B.: Linear dependent types in a call-by-value scenario. In: ACM PPDP 2012. pp. 115--126 (2012)
[14]
Danos, V., Regnier, L.: Reversible, irreversible and optimal lambdamachines. Theor. Comput. Sci. 227(1-2), 79--97 (1999)
[15]
Denney, E.: Refinement types for specification. In: IFIP-PROCOMET. pp. 148--166 (1998)
[16]
Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine and the _-calculus. Tech. Rep. 197, Computer Science Department, Indiana University (1986)
[17]
Ghica, D.R.: Slot games: a quantitative model of computation. In: ACM POPL 2005. pp. 85--97 (2005)
[18]
Ghica, D.R., Smith, A.: Geometry of synthesis III: resource management through type inference. In: ACM POPL 2011. pp. 345--356 (2011)
[19]
Girard, J.Y., Scedrov, A., Scott, P.: Bounded linear logic. Theor. Comp. Sci. 97(1), 1--66 (1992)
[20]
Gulwani, S.: Speed: Symbolic complexity bound analysis. In: CAV. pp. 51--62 (2009)
[21]
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis. In: ACM POPL 2011. pp. 357--370 (2011)
[22]
Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: ACM POPL 1996. pp. 410--423 (1996)
[23]
Jost, S., Hammond, K., Loidl, H.W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: ACM POPL 2010. Madrid, Spain (2010)
[24]
Krivine, J.L.: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3), 199--207 (2007)
[25]
Maraist, J., Odersky, M., Turner, D.N.,Wadler, P.: Call-by-name, callby- value, call-by-need and the linear lambda calculus. Electr. Notes Theor. Comput. Sci. 1, 370--392 (1995)
[26]
Plotkin, G.D.: LCF considerd as a programming language. Theor. Comp. Sci. 5, 225--255 (1977)
[27]
Sands, D.: Complexity analysis for a lazy higher-order language. In: ESOP 1990. LNCS, vol. 432, pp. 361--376 (1990)
[28]
Sands, D.: Operational theories of improvement in functional languages (extended abstract). In: Functional Programming. pp. 298--311 (1991)
[29]
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., Stenstrom, P.: The worst case execution time problem - overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. (2008)

Cited By

View all
  • (2025)Flexible Type-Based Resource Estimation in Quantum Circuit Description LanguagesProceedings of the ACM on Programming Languages10.1145/37048839:POPL(1386-1416)Online publication date: 9-Jan-2025
  • (2024)Circuit Width Estimation via Effect Typing and Linear DependencyProgramming Languages and Systems10.1007/978-3-031-57267-8_1(3-30)Online publication date: 5-Apr-2024
  • (2022)Differential cost analysis with simultaneous potentials and anti-potentialsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523435(442-457)Online publication date: 9-Jun-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2013
586 pages
ISBN:9781450318327
DOI:10.1145/2429069
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 48, Issue 1
    POPL '13
    January 2013
    561 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2480359
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. complexity analysis
  2. functional programming
  3. higher-order types
  4. linear logic
  5. resource consumption

Qualifiers

  • Research-article

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)8
  • Downloads (Last 6 weeks)1
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Flexible Type-Based Resource Estimation in Quantum Circuit Description LanguagesProceedings of the ACM on Programming Languages10.1145/37048839:POPL(1386-1416)Online publication date: 9-Jan-2025
  • (2024)Circuit Width Estimation via Effect Typing and Linear DependencyProgramming Languages and Systems10.1007/978-3-031-57267-8_1(3-30)Online publication date: 5-Apr-2024
  • (2022)Differential cost analysis with simultaneous potentials and anti-potentialsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523435(442-457)Online publication date: 9-Jun-2022
  • (2020)Raising expectations: automating expected cost analysis with typesProceedings of the ACM on Programming Languages10.1145/34089924:ICFP(1-31)Online publication date: 3-Aug-2020
  • (2020)Tight typings and split bounds, fully developedJournal of Functional Programming10.1017/S095679682000012X30Online publication date: 19-May-2020
  • (2019)Type-Driven Verification of Non-functional PropertiesProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354171(1-15)Online publication date: 7-Oct-2019
  • (2019)Bidirectional type checking for relational propertiesProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314603(533-547)Online publication date: 8-Jun-2019
  • (2019)Type-guided worst-case input generationProceedings of the ACM on Programming Languages10.1145/32903263:POPL(1-30)Online publication date: 2-Jan-2019
  • (2018)Bounded expectations: resource analysis for probabilistic programsACM SIGPLAN Notices10.1145/3296979.319239453:4(496-512)Online publication date: 11-Jun-2018
  • (2018)Work Analysis with Resource-Aware Session TypesProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209146(305-314)Online publication date: 9-Jul-2018
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media