More Web Proxy on the site http://driver.im/

research-article

Open access

A unifying type-theory for higher-order (amortized) cost analysis

Authors:

Marco Gaboardi,

Jan HoffmannAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 27, Pages 1 - 28

https://doi.org/10.1145/3434308

Published: 04 January 2021 Publication History

Abstract

This paper presents λ-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it. λ-amor introduces a new modal type for representing potentials – costs that have been accounted for, but not yet incurred, which are central to amortized analysis. Additionally, λ-amor relies on standard type-theoretic concepts like affineness, refinement types and an indexed cost monad. λ-amor is proved sound using a rather simple logical relation. We embed two existing type systems for cost analysis in λ-amor showing that, despite its simplicity, λ-amor can simulate cost analysis for different evaluation strategies (call-by-name and call-by-value), in different styles (effect-based and coeffect-based), and with or without amortization. One of the embeddings also implies that λ-amor is relatively complete for all terminating PCF programs.

References

[1]

Amal Jamil Ahmed. 2004. Semantics of types for mutable state. Ph.D. Dissertation. Princeton university.

Digital Library

[2]

Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Annual ACM/IEEE Symposium on Logic in Computer Science.

[3]

Martin Avanzini and Ugo Dal Lago. 2017. Automating Sized-type Inference for Complexity Analysis. Proc. ACM Program. Lang. 1, ICFP ( 2017 ).

Digital Library

[4]

Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coefect Calculus. In Proceedings of the European Symposium on Programming Languages and Systems.

Digital Library

[5]

Quentin Carbonneaux, Jan Hofmann, and Zhong Shao. 2015. Compositional certified resource bounds. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[6]

Arthur Charguéraud and François Pottier. 2019. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. J. Autom. Reasoning 62, 3 ( 2019 ).

Digital Library

[7]

Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hofmann. 2017. Relational cost analysis. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[8]

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliford Stein. 2009. Introduction to Algorithms, 3rd Edition. MIT Press.

Digital Library

[9]

Karl Crary and Stephanie Weirich. 2000. Resource Bound Certification. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[10]

Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8, 4 ( 2011 ).

[11]

Ugo Dal Lago and Barbara Petit. 2012. Linear Dependent Types in a Call-by-value Scenario. Science of Computer Programming 84 ( 2012 ).

[12]

Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[13]

Norman Danner, Daniel R. Licata, and Ramyaa. 2015. Denotational cost semantics for functional languages with inductive types. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming. 140-151.

Digital Library

[14]

Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining Efects and Coefects via Grading. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming.

Digital Library

[15]

Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science 97, 1 ( 1992 ).

[16]

Martin A. T. Handley, Niki Vazou, and Graham Hutton. 2020. Liquidate your assets: reasoning about resource usage in liquid Haskell. Proc. ACM Program. Lang. 4, POPL ( 2020 ).

Digital Library

[17]

Maximilian P. L. Haslbeck and Tobias Nipkow. 2018. Hoare Logics for Time Bounds-A Study in Meta Theory. In Tools and Algorithms for the Construction and Analysis of Systems, Vol. 10805.

[18]

Jan Hofman. 2011. Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Ph.D. Dissertation. Ludwig-Maximilians-Universität München.

[19]

Jan Hofmann, Klaus Aehlig, and Martin Hofmann. 2011. Multivariate Amortized Resource Analysis. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[20]

Jan Hofmann, Ankush Das, and Shu-Chun Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages.

Digital Library

[21]

Jan Hofmann and Martin Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential: A Static Inference of Polynomial Bounds for Functional Programs. In Proceedings of the European Conference on Programming Languages and Systems.

Digital Library

[22]

Martin Hofmann and Stefen Jost. 2003. Static Prediction of Heap Space Usage for First-order Functional Programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[23]

Stefen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-order Programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[24]

Stefen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, and Martin Hofmann. 2009. "Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis. In Proceedings of Formal Methods.

Digital Library

[25]

Stefen Jost, Pedro Vasconcelos, Mário Florido, and Kevin Hammond. 2017. Type-Based Cost Analysis for Lazy Functional Languages. J. Autom. Reason. 59, 1 ( 2017 ).

Digital Library

[26]

G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. 2020. Recurrence extraction for functional programs through call-by-push-value. Proc. ACM Program. Lang. 4, POPL ( 2020 ).

Digital Library

[27]

Tristan Knoth, Di Wang, Nadia Polikarpova, and Jan Hofmann. 2019. Resource-guided program synthesis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[28]

Jean-Louis Krivine. 2007. A Call-by-name Lambda-calculus Machine. Higher Order Symbolic Computation 20, 3 ( 2007 ).

[29]

Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. 2017. Contract-based Resource Verification for Higher-order Functions with Memoization. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages.

Digital Library

[30]

Dylan McDermott and Alan Mycroft. 2018. Call-by-need efects via coefects. Open Comput. Sci. 8, 1 ( 2018 ).

[31]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2019. Time credits and time receipts in Iris. In European Symposium on Programming.

[32]

Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation 93, 1 ( 1991 ).

[33]

Georg Neis, Derek Dreyer, and Andreas Rossberg. 2011. Non-parametric parametricity. J. Funct. Program. 21, 4-5 ( 2011 ).

Digital Library

[34]

Chris Okasaki. 1996. Purely Functional Data Structures. Ph.D. Dissertation. Carnegie Mellon University.

Digital Library

[35]

Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2014. Coefects: A Calculus of Context-dependent Computation. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming.

Digital Library

[36]

Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2013. Coefects: Unified Static Analysis of Context-Dependence. In Automata, Languages, and Programming-International Colloquium.

[37]

David J. Pym, Peter W. O'Hearn, and Hongseok Yang. 2004. Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315, 1 ( 2004 ).

[38]

Robert E. Tarjan. 1985. Amortized computational complexity. SIAM J. Algebraic Discrete Methods 6, 2 ( 1985 ).

[39]

Hongwei Xi. 2007. Dependent ML An approach to practical programming with dependent types. J. Funct. Program. 17, 2 ( 2007 ).

Digital Library

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Xia LIsrael LKramarz MColtharp NClaessen KWeirich SLi Y(2024)Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy ProgramsProceedings of the ACM on Programming Languages10.1145/36746268:ICFP(30-63)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674626
Show More Cited By

Index Terms

A unifying type-theory for higher-order (amortized) cost analysis
1. Theory of computation
  1. Logic
    1. Linear logic
    2. Type theory
  2. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Formalizing Type Operations Using the “Image” Type Constructor

In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper ...
Inductive Types in Homotopy Type Theory
LICS '12: Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science

Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of ...
A sequent calculus for type theory
CSL'06: Proceedings of the 20th international conference on Computer Science Logic

Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent Calculi (PTSC) by enriching a sequent calculus due to Herbelin, adapted ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
1,034
Total Downloads

Downloads (Last 12 months)246
Downloads (Last 6 weeks)27

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Xia LIsrael LKramarz MColtharp NClaessen KWeirich SLi Y(2024)Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy ProgramsProceedings of the ACM on Programming Languages10.1145/36746268:ICFP(30-63)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674626
Atkey R(2024)Polynomial Time and Dependent TypesProceedings of the ACM on Programming Languages10.1145/36329188:POPL(2288-2317)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632918
Grodin HNiu YSterling JHarper R(2024)Decalf: A Directed, Effectful Cost-Aware Logical FrameworkProceedings of the ACM on Programming Languages10.1145/36328528:POPL(273-301)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632852
Batz KKaminski BKatoen JMatheja CVerscht L(2023)A Calculus for Amortized Expected RuntimesProceedings of the ACM on Programming Languages10.1145/35712607:POPL(1957-1986)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571260
Grosen JKahn DHoffmann J(2023)Automatic Amortized Resource Analysis with Regular Recursive Types2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175720(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175720
Suzanne HChailloux E(2023)A Reusable Machine-Calculus for Automated Resource AnalysesLogic-Based Program Synthesis and Transformation10.1007/978-3-031-45784-5_5(61-79)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45784-5_5
Haeri SThompson PDavies NVan Roy PHammond KChapman J(2022)Mind Your Outcomes: The ΔQSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case StudyComputers10.3390/computers1103004511:3(45)Online publication date: 17-Mar-2022
https://doi.org/10.3390/computers11030045
Niu YSterling JGrodin HHarper R(2022)A cost-aware logical frameworkProceedings of the ACM on Programming Languages10.1145/34986706:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498670
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents