{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T16:55:30Z","timestamp":1787504130391,"version":"build-2736575974"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["AA Contract FA8750-18-C-0092"],"award-info":[{"award-number":["AA Contract FA8750-18-C-0092"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Science Foundation","doi-asserted-by":"publisher","award":["SaTC Award 1801369,CAREER Award 1845514,SHF Award 1812876, SHF Award 2007784"],"award-info":[{"award-number":["SaTC Award 1801369,CAREER Award 1845514,SHF Award 1812876, SHF Award 2007784"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,8,2]]},"abstract":"<jats:p>This article presents a type-based analysis for deriving upper bounds on the expected execution cost of probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher-order functions and inductive data types. The derived bounds are multivariate polynomials that are functions of data structures. Bound inference is enabled by local type rules that reduce type inference to linear constraint solving. The type system is based on the potential method of amortized analysis and extends automatic amortized resource analysis (AARA) for deterministic programs. A main innovation is that bounds can contain symbolic probabilities, which may appear in data structures and function arguments. Another contribution is a novel soundness proof that establishes the correctness of the derived bounds with respect to a distribution-based operational cost semantics that also includes nontrivial diverging behavior. For cost models like time, derived bounds imply termination with probability one. To highlight the novel ideas, the presentation focuses on linear potential and a core language. However, the analysis is implemented as an extension of Resource Aware ML and supports polynomial bounds and user defined data structures. The effectiveness of the technique is evaluated by analyzing the sample complexity of discrete distributions and with a novel average-case estimation for deterministic programs that combines expected cost analysis with statistical methods.<\/jats:p>","DOI":"10.1145\/3408992","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T09:48:02Z","timestamp":1596448082000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Raising expectations: automating expected cost analysis with types"],"prefix":"10.1145","volume":"4","author":[{"given":"Di","family":"Wang","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David M.","family":"Kahn","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"E. Albert P. Arenas S. Genaim M. G\u00f3mez-Zamalloa G. Puebla D. Ram\u00edrez G. Rom\u00e1n and D. Zanardini. 2009. Termination and Cost Analysis with COSTA and its User Interfaces. Electr. Notes Theor. Comp. Sci. 258 ( December 2009 ). Issue 1.  E. Albert P. Arenas S. Genaim M. G\u00f3mez-Zamalloa G. Puebla D. Ram\u00edrez G. Rom\u00e1n and D. Zanardini. 2009. Termination and Cost Analysis with COSTA and its User Interfaces. Electr. Notes Theor. Comp. Sci. 258 ( December 2009 ). Issue 1.","DOI":"10.1016\/j.entcs.2009.12.008"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"E. Albert J. C. Fern\u00e1ndez and G. Rom\u00e1n-D\u00edez. 2015. Non-cumulative Resource Analysis. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'15).  E. Albert J. C. Fern\u00e1ndez and G. Rom\u00e1n-D\u00edez. 2015. Non-cumulative Resource Analysis. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'15).","DOI":"10.1007\/978-3-662-46681-0_6"},{"key":"e_1_2_2_3_1","volume-title":"Amortised Resource Analysis with Separation Logic. In European Symp. on Programming (ESOP'10)","author":"Atkey R.","year":"2010","unstructured":"R. Atkey . 2010 . Amortised Resource Analysis with Separation Logic. In European Symp. on Programming (ESOP'10) . R. Atkey. 2010. Amortised Resource Analysis with Separation Logic. In European Symp. on Programming (ESOP'10)."},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"M. Avanzini U. Dal Lago and A. Ghyselen. 2019. Type-Based Complexity Analysis of Probabilistic Functional Programs. In Logic in Computer Science (LICS'19).  M. Avanzini U. Dal Lago and A. Ghyselen. 2019. Type-Based Complexity Analysis of Probabilistic Functional Programs. In Logic in Computer Science (LICS'19).","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_2_2_5_1","volume-title":"Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Int. Conf. on Functional Programming (ICFP'15)","author":"Avanzini M.","unstructured":"M. Avanzini , U. Dal Lago , and G. Moser . 2015 . Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Int. Conf. on Functional Programming (ICFP'15) . M. Avanzini, U. Dal Lago, and G. Moser. 2015. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Int. Conf. on Functional Programming (ICFP'15)."},{"key":"e_1_2_2_6_1","volume-title":"Int. Conf. on Rewriting Techniques and Applications (RTA'13)","author":"Avanzini M.","unstructured":"M. Avanzini and G. Moser . 2013. A Combination Framework for Complexity . In Int. Conf. on Rewriting Techniques and Applications (RTA'13) . M. Avanzini and G. Moser. 2013. A Combination Framework for Complexity. In Int. Conf. on Rewriting Techniques and Applications (RTA'13)."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411509.1411514"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"G. Barthe B. Gr\u00e9goire and S. Zanella B\u00e9guelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Princ. of Prog. Lang. (POPL'09).  G. Barthe B. Gr\u00e9goire and S. Zanella B\u00e9guelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Princ. of Prog. Lang. (POPL'09).","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"G. Barthe B. K\u00f6pf F. Olmedo and S. Zanella B\u00e9guelin. 2012. Probabilistic Relational Reasoning for Diferential Privacy. In Princ. of Prog. Lang. (POPL'12).  G. Barthe B. K\u00f6pf F. Olmedo and S. Zanella B\u00e9guelin. 2012. Probabilistic Relational Reasoning for Diferential Privacy. In Princ. of Prog. Lang. (POPL'12).","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_2_2_10_1","volume-title":"European Symp. on Programming (ESOP'18)","author":"Batz Kevin","unstructured":"Kevin Batz , B. L. Kaminski , J.-P. Katoen , and C. Matheja . 2018. How long, O Bayesian network, will I sample thee? . In European Symp. on Programming (ESOP'18) . Kevin Batz, B. L. Kaminski, J.-P. Katoen, and C. Matheja. 2018. How long, O Bayesian network, will I sample thee?. In European Symp. on Programming (ESOP'18)."},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"S. Bhat A. Agarwal R. Vuduc and A. Gray. 2012. A Type Theory for Probability Density Functions. In Princ. of Prog. Lang. (POPL'12).  S. Bhat A. Agarwal R. Vuduc and A. Gray. 2012. A Type Theory for Probability Density Functions. In Princ. of Prog. Lang. (POPL'12).","DOI":"10.1145\/2103656.2103721"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"S. Bhat J. Borgstr\u00f6m A. D. Gordon and C. Russo. 2013. Deriving probability density functions from probabilistic functional programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'13).  S. Bhat J. Borgstr\u00f6m A. D. Gordon and C. Russo. 2013. Deriving probability density functions from probabilistic functional programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'13).","DOI":"10.1007\/978-3-642-36742-7_35"},{"key":"e_1_2_2_13_1","volume-title":"Probability and Measure","author":"Billingsley P.","unstructured":"P. Billingsley . 2012. Probability and Measure . John Wiley & Sons, Inc. P. Billingsley. 2012. Probability and Measure. John Wiley & Sons, Inc."},{"key":"e_1_2_2_14_1","volume-title":"ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning (LPAR'10).","author":"Blanc R.","year":"2010","unstructured":"R. Blanc , T. A. Henzinger , T. Hottelier , and L. Kov\u00e1cs . 2010 . ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning (LPAR'10). R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kov\u00e1cs. 2010. ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning (LPAR'10)."},{"key":"e_1_2_2_15_1","volume-title":"Int. Conf. on Functional Programming (ICFP'16)","author":"Borgstr\u00f6m J.","unstructured":"J. Borgstr\u00f6m , U. Dal Lago , A. D. Gordon , and M. Szymczak . 2016. A Lambda-Calculus Foundation for Universal Probabilistic Programming . In Int. Conf. on Functional Programming (ICFP'16) . J. Borgstr\u00f6m, U. Dal Lago, A. D. Gordon, and M. Szymczak. 2016. A Lambda-Calculus Foundation for Universal Probabilistic Programming. In Int. Conf. on Functional Programming (ICFP'16)."},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"M. Brockschmidt F. Emmes S. Falke C. Fuhs and J. Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'14).  M. Brockschmidt F. Emmes S. Falke C. Fuhs and J. Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'14).","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"e_1_2_2_17_1","volume-title":"WISE: Automated Test Generation for Worst-case Complexity. In Int. Conf. on Softw. Eng. (ICSE'09)","author":"Burnim J.","unstructured":"J. Burnim , S. Juvekar , and K. Sen . 2009 . WISE: Automated Test Generation for Worst-case Complexity. In Int. Conf. on Softw. Eng. (ICSE'09) . J. Burnim, S. Juvekar, and K. Sen. 2009. WISE: Automated Test Generation for Worst-case Complexity. In Int. Conf. on Softw. Eng. (ICSE'09)."},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Q. Carbonneaux J. Hofmann T. Reps and Z. Shao. 2017. Automated Resource Analysis with Coq Proof Objects. In Computer Aided Verif. (CAV'17).  Q. Carbonneaux J. Hofmann T. Reps and Z. Shao. 2017. Automated Resource Analysis with Coq Proof Objects. In Computer Aided Verif. (CAV'17).","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Q. Carbonneaux J. Hofmann and Z. Shao. 2015. Compositional Certified Resource Bounds. In Prog. Lang. Design and Impl. (PLDI'15).  Q. Carbonneaux J. Hofmann and Z. Shao. 2015. Compositional Certified Resource Bounds. In Prog. Lang. Design and Impl. (PLDI'15).","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_2_20_1","volume-title":"Stan: A Probabilistic Programming Language. J. Statistical Softw. 76 ( 2017 ). Issue 1.","author":"Carpenter B.","year":"2017","unstructured":"B. Carpenter , A. Gelman , M. D. Hofman , D. Lee , B. Goodrich , M. Betancourt , M. Brubaker , J. Guo , P. Li , and A. Riddell . 2017 . Stan: A Probabilistic Programming Language. J. Statistical Softw. 76 ( 2017 ). Issue 1. B. Carpenter, A. Gelman, M. D. Hofman, D. Lee, B. Goodrich, M. Betancourt, M. Brubaker, J. Guo, P. Li, and A. Riddell. 2017. Stan: A Probabilistic Programming Language. J. Statistical Softw. 76 ( 2017 ). Issue 1."},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"A. Chargu\u00e9raud and F. Pottier. 2015. Machine-Checked Verification of the Correctness and Amortized Complexity of an Eficient Union-Find Implementation. In Interactive Theorem Proving (ITP'15).  A. Chargu\u00e9raud and F. Pottier. 2015. Machine-Checked Verification of the Correctness and Amortized Complexity of an Eficient Union-Find Implementation. In Interactive Theorem Proving (ITP'15).","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee H. Fu and A. K. Goharshady. 2016a. Termination Analysis of Probabilistic Programs Through Positivstellensatz's. In Computer Aided Verif. (CAV'16).  K. Chatterjee H. Fu and A. K. Goharshady. 2016a. Termination Analysis of Probabilistic Programs Through Positivstellensatz's. In Computer Aided Verif. (CAV'16).","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee H. Fu P. Novotn\u00fd and R. Hasheminezhad. 2016b. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Afine Probabilistic Programs. In Princ. of Prog. Lang. (POPL'16).  K. Chatterjee H. Fu P. Novotn\u00fd and R. Hasheminezhad. 2016b. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Afine Probabilistic Programs. In Princ. of Prog. Lang. (POPL'16).","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_2_24_1","volume-title":"Int. Conf. on Softw. Eng. (ICSE'16)","author":"Chen B.","unstructured":"B. Chen , Y. Liu , and W. Le . 2016. Generating Performance Distributions via Probabilistic Symbolic Execution . In Int. Conf. on Softw. Eng. (ICSE'16) . B. Chen, Y. Liu, and W. Le. 2016. Generating Performance Distributions via Probabilistic Symbolic Execution. In Int. Conf. on Softw. Eng. (ICSE'16)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"E. \u00c7i\u00e7ek G. Barthe M. Gaboardi D. Garg and J. Hofmann. 2017. Relational Cost Analysis. In Princ. of Prog. Lang. (POPL'17).  E. \u00c7i\u00e7ek G. Barthe M. Gaboardi D. Garg and J. Hofmann. 2017. Relational Cost Analysis. In Princ. of Prog. Lang. (POPL'17).","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_2_26_1","volume-title":"Refinement Types for Incremental Computational Complexity. In European Symp. on Programming (ESOP'15)","author":"\u00c7i\u00e7ek E.","unstructured":"E. \u00c7i\u00e7ek , D. Garg , and U. A. Acar . 2015 . Refinement Types for Incremental Computational Complexity. In European Symp. on Programming (ESOP'15) . E. \u00c7i\u00e7ek, D. Garg, and U. A. Acar. 2015. Refinement Types for Incremental Computational Complexity. In European Symp. on Programming (ESOP'15)."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsif.2008.0014"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"K. Crary and S. Weirich. 2000. Resource Bound Certification. In Princ. of Prog. Lang. (POPL'00).  K. Crary and S. Weirich. 2000. Resource Bound Certification. In Princ. of Prog. Lang. (POPL'00).","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"J. Da Silva and J. G. Stefan. 2006. A Probabilistic Pointer Analysis for Speculative Optimizations. In Architectural Support for Prog. Lang. and Op. Syst. (ASPLOS'06).  J. Da Silva and J. G. Stefan. 2006. A Probabilistic Pointer Analysis for Speculative Optimizations. In Architectural Support for Prog. Lang. and Op. Syst. (ASPLOS'06).","DOI":"10.1145\/1168857.1168908"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"U. Dal Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS'11).  U. Dal Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS'11).","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_2_31_1","volume-title":"On Linear Dependent Types and Probabilistic Termination. In International Workshop on Developments in Implicit Computational Complexity.","author":"Dal Lago U.","unstructured":"U. Dal Lago and A. Ghyselen . 2018 . On Linear Dependent Types and Probabilistic Termination. In International Workshop on Developments in Implicit Computational Complexity. U. Dal Lago and A. Ghyselen. 2018. On Linear Dependent Types and Probabilistic Termination. In International Workshop on Developments in Implicit Computational Complexity."},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"U. Dal Lago and C. Grellois. 2019. Probabilistic Termination by Monadic Afine Sized Typing. Trans. on Prog. Lang. and Syst. 41 ( June 2019 ). Issue 2.  U. Dal Lago and C. Grellois. 2019. Probabilistic Termination by Monadic Afine Sized Typing. Trans. on Prog. Lang. and Syst. 41 ( June 2019 ). Issue 2.","DOI":"10.1145\/3293605"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"U. Dal Lago and B. Petit. 2013. The Geometry of Types. In Princ. of Prog. Lang. (POPL'13).  U. Dal Lago and B. Petit. 2013. The Geometry of Types. In Princ. of Prog. Lang. (POPL'13).","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"N. A. Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Princ. of Prog. Lang. (POPL'08).  N. A. Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In Princ. of Prog. Lang. (POPL'08).","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_2_35_1","volume-title":"Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP'15)","author":"Danner N.","unstructured":"N. Danner , D. R. Licata , and R. Ramyaa . 2015 . Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP'15) . N. Danner, D. R. Licata, and R. Ramyaa. 2015. Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP'15)."},{"key":"e_1_2_2_36_1","unstructured":"D. Djuric. 2019. Billions of Random Numbers in a Blink of an Eye. Available on https:\/\/dragan.rocks\/articles\/19\/Billionrandom-numbers-blink-eye-Clojure.  D. Djuric. 2019. Billions of Random Numbers in a Blink of an Eye. Available on https:\/\/dragan.rocks\/articles\/19\/Billionrandom-numbers-blink-eye-Clojure."},{"key":"e_1_2_2_37_1","volume-title":"Reliability Analysis in Symbolic Pathfinder. In Int. Conf. on Softw. Eng. (ICSE'13)","author":"Filieri A.","unstructured":"A. Filieri , C. S. P\u0103s\u0103reanu , and W. Visser . 2013 . Reliability Analysis in Symbolic Pathfinder. In Int. Conf. on Softw. Eng. (ICSE'13) . A. Filieri, C. S. P\u0103s\u0103reanu, and W. Visser. 2013. Reliability Analysis in Symbolic Pathfinder. In Int. Conf. on Softw. Eng. (ICSE'13)."},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"A. Filieri C. S. P\u0103s\u0103reanu W. Visser and J. Geldenhuys. 2014. Statistical Symbolic Execution with Informed Sampling. In Found. of Softw. Eng. (FSE'14).  A. Filieri C. S. P\u0103s\u0103reanu W. Visser and J. Geldenhuys. 2014. Statistical Symbolic Execution with Informed Sampling. In Found. of Softw. Eng. (FSE'14).","DOI":"10.1145\/2635868.2635899"},{"key":"e_1_2_2_39_1","volume-title":"Resource Analysis of Complex Programs with Cost Equations. In Asian Symp. on Prog. Lang. and Systems (APLAS'14)","author":"Flores-Montoya A.","unstructured":"A. Flores-Montoya and R. H\u00e4hnle . 2014 . Resource Analysis of Complex Programs with Cost Equations. In Asian Symp. on Prog. Lang. and Systems (APLAS'14) . A. Flores-Montoya and R. H\u00e4hnle. 2014. Resource Analysis of Complex Programs with Cost Equations. In Asian Symp. on Prog. Lang. and Systems (APLAS'14)."},{"key":"e_1_2_2_40_1","volume-title":"Lower Runtime Bounds for Integer Programs. In Int. Joint Conf. on Automated Reasoning (IJCAR'16)","author":"Frohn F.","unstructured":"F. Frohn , M. Naaf , J. Hensel , M. Brockschmidt , and J. Giesl . 2016 . Lower Runtime Bounds for Integer Programs. In Int. Joint Conf. on Automated Reasoning (IJCAR'16) . F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt, and J. Giesl. 2016. Lower Runtime Bounds for Integer Programs. In Int. Joint Conf. on Automated Reasoning (IJCAR'16)."},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"M. Gaboardi A. Haeberlen J. Hsu A. Narayan and B. C. Pierce. 2013. Linear Dependent Types for Diferential Privacy. In Princ. of Prog. Lang. (POPL'13).  M. Gaboardi A. Haeberlen J. Hsu A. Narayan and B. C. Pierce. 2013. Linear Dependent Types for Diferential Privacy. In Princ. of Prog. Lang. (POPL'13).","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_42_1","unstructured":"N. D. Goodman and A. Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. Available on http:\/\/dippl.org.  N. D. Goodman and A. Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. Available on http:\/\/dippl.org."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_2_44_1","volume-title":"SPEED: Symbolic Complexity Bound Analysis. In Computer Aided Verif. (CAV'09).","author":"Gulwani S.","year":"2009","unstructured":"S. Gulwani . 2009 . SPEED: Symbolic Complexity Bound Analysis. In Computer Aided Verif. (CAV'09). S. Gulwani. 2009. SPEED: Symbolic Complexity Bound Analysis. In Computer Aided Verif. (CAV'09)."},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"M. Hark B. L. Kaminski J. Giesl and J.-P. Katoen. 2020. Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification. In Princ. of Prog. Lang. (POPL'20).  M. Hark B. L. Kaminski J. Giesl and J.-P. Katoen. 2020. Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification. In Princ. of Prog. Lang. (POPL'20).","DOI":"10.1145\/3371105"},{"key":"e_1_2_2_46_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper R.","unstructured":"R. Harper . 2016. Practical Foundations for Programming Languages . Cambridge University Press . R. Harper. 2016. Practical Foundations for Programming Languages. Cambridge University Press."},{"key":"e_1_2_2_47_1","doi-asserted-by":"crossref","unstructured":"J. Hofmann K. Aehlig and M. Hofmann. 2011. Multivariate Amortized Resource Analysis. In Princ. of Prog. Lang. (POPL'11).  J. Hofmann K. Aehlig and M. Hofmann. 2011. Multivariate Amortized Resource Analysis. In Princ. of Prog. Lang. (POPL'11).","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"J. Hofmann A. Das and S.-C. Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Princ. of Prog. Lang. (POPL'17).  J. Hofmann A. Das and S.-C. Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Princ. of Prog. Lang. (POPL'17).","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_2_49_1","volume-title":"Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In Asian Symp. on Prog. Lang. and Systems (APLAS'10)","author":"Hofmann J.","unstructured":"J. Hofmann and M. Hofmann . 2010a . Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In Asian Symp. on Prog. Lang. and Systems (APLAS'10) . J. Hofmann and M. Hofmann. 2010a. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In Asian Symp. on Prog. Lang. and Systems (APLAS'10)."},{"key":"e_1_2_2_50_1","volume-title":"Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP'10)","author":"Hofmann J.","unstructured":"J. Hofmann and M. Hofmann . 2010b . Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP'10) . J. Hofmann and M. Hofmann. 2010b. Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP'10)."},{"key":"e_1_2_2_51_1","doi-asserted-by":"crossref","unstructured":"M. Hofmann and S. Jost. 2003. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Princ. of Prog. Lang. (POPL'03).  M. Hofmann and S. Jost. 2003. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Princ. of Prog. Lang. (POPL'03).","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_2_52_1","volume-title":"Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA'15)","author":"Hofmann M.","unstructured":"M. Hofmann and G. Moser . 2015 . Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA'15) . M. Hofmann and G. Moser. 2015. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA'15)."},{"key":"e_1_2_2_53_1","unstructured":"M. Hofmann and G. Moser. 2018. Analysis of Logarithmic Amortised Complexity. Technical Report. Computing Research Repository.  M. Hofmann and G. Moser. 2018. Analysis of Logarithmic Amortised Complexity. Technical Report. Computing Research Repository."},{"key":"e_1_2_2_54_1","doi-asserted-by":"crossref","unstructured":"S. Jost K. Hammond H.-W. Loidl and M. Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In Princ. of Prog. Lang. (POPL'10).  S. Jost K. Hammond H.-W. Loidl and M. Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In Princ. of Prog. Lang. (POPL'10).","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_2_55_1","volume-title":"Symp. on Form. Meth. (FM'09)","author":"Jost S.","unstructured":"S. Jost , H.-W. Loidl , K. Hammond , N. Scaife , and M. Hofmann . 2009. Carbon Credits for Resource-Bounded Computations using Amortised Analysis . In Symp. on Form. Meth. (FM'09) . S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. 2009. Carbon Credits for Resource-Bounded Computations using Amortised Analysis. In Symp. on Form. Meth. (FM'09)."},{"key":"e_1_2_2_56_1","volume-title":"Exponential Automatic Amortized Resource Analysis. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20)","author":"Kahn D. M.","unstructured":"D. M. Kahn and J. Hofmann . 2020 . Exponential Automatic Amortized Resource Analysis. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20) . D. M. Kahn and J. Hofmann. 2020. Exponential Automatic Amortized Resource Analysis. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20)."},{"key":"e_1_2_2_57_1","volume-title":"Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In European Symp. on Programming (ESOP'16)","author":"Kaminski B. L.","unstructured":"B. L. Kaminski , J.-P. Katoen , C. Matheja , and F. Olmedo . 2016 . Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In European Symp. on Programming (ESOP'16) . B. L. Kaminski, J.-P. Katoen, C. Matheja, and F. Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In European Symp. on Programming (ESOP'16)."},{"key":"e_1_2_2_58_1","doi-asserted-by":"crossref","unstructured":"G. A. Kavvos E. Morehouse D. R. Licata and N. Danner. 2020. Recurrence Extraction for Functional Programs through Call-by-Push-Value. In Princ. of Prog. Lang. (POPL'20).  G. A. Kavvos E. Morehouse D. R. Licata and N. Danner. 2020. Recurrence Extraction for Functional Programs through Call-by-Push-Value. In Princ. of Prog. Lang. (POPL'20).","DOI":"10.1145\/3371083"},{"key":"e_1_2_2_59_1","doi-asserted-by":"crossref","unstructured":"Z. Kincaid J. Breck A. F. Boroujeni and T. Reps. 2017. Compositional Recurrence Analysis Revisited. In Prog. Lang. Design and Impl. (PLDI'17).  Z. Kincaid J. Breck A. F. Boroujeni and T. Reps. 2017. Compositional Recurrence Analysis Revisited. In Prog. Lang. Design and Impl. (PLDI'17).","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_2_60_1","doi-asserted-by":"crossref","unstructured":"T. Knoth D. Wang N. Polikarpova and J. Hofmann. 2019. Resource-Guided Program Synthesis. In Prog. Lang. Design and Impl. (PLDI'19).  T. Knoth D. Wang N. Polikarpova and J. Hofmann. 2019. Resource-Guided Program Synthesis. In Prog. Lang. Design and Impl. (PLDI'19).","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_2_2_61_1","unstructured":"Donald Knuth and Andrew Yao. 1976. Algorithms and Complexity: New Directions and Recent Results chapter The complexity of nonuniform random number generation.  Donald Knuth and Andrew Yao. 1976. Algorithms and Complexity: New Directions and Recent Results chapter The complexity of nonuniform random number generation."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_63_1","doi-asserted-by":"crossref","unstructured":"S. Kura N. Urabe and I. Hasuo. 2019. Tail Probability for Randomized Program Runtimes via Martingales for Higher Moments. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'19).  S. Kura N. Urabe and I. Hasuo. 2019. Tail Probability for Randomized Program Runtimes via Martingales for Higher Moments. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'19).","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_2_2_64_1","doi-asserted-by":"crossref","unstructured":"A. K. Lew M. F. Cusumano-Towner B. Sherman M. Carbin and V. K. Mansinghka. 2020. Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages. In Princ. of Prog. Lang. (POPL'20).  A. K. Lew M. F. Cusumano-Towner B. Sherman M. Carbin and V. K. Mansinghka. 2020. Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages. In Princ. of Prog. Lang. (POPL'20).","DOI":"10.1145\/3371087"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1088\/0004-637X\/721\/2\/1014"},{"key":"e_1_2_2_66_1","doi-asserted-by":"crossref","unstructured":"V. K. Mansinghka U. Schaechtle S. Handa A. Radul Y. Chen and M. C. Rinard. 2018. Probabilistic Programming with Programmable Inference. In Prog. Lang. Design and Impl. (PLDI'18).  V. K. Mansinghka U. Schaechtle S. Handa A. Radul Y. Chen and M. C. Rinard. 2018. Probabilistic Programming with Programmable Inference. In Prog. Lang. Design and Impl. (PLDI'18).","DOI":"10.1145\/3192366.3192409"},{"key":"e_1_2_2_67_1","doi-asserted-by":"crossref","unstructured":"A. K. McIver and C. C. Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. Springer Science+Business Media Inc.  A. K. McIver and C. C. Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. Springer Science+Business Media Inc.","DOI":"10.1145\/1059816.1059824"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-1996(83)90017-X"},{"key":"e_1_2_2_69_1","volume-title":"Bounded Expectations: Resource Analysis for Probabilistic Programs. In Prog. Lang. Design and Impl. (PLDI'18).","author":"Ngo V. C.","year":"2018","unstructured":"V. C. Ngo , Q. Carbonneaux , and J. Hofmann . 2018 . Bounded Expectations: Resource Analysis for Probabilistic Programs. In Prog. Lang. Design and Impl. (PLDI'18). V. C. Ngo, Q. Carbonneaux, and J. Hofmann. 2018. Bounded Expectations: Resource Analysis for Probabilistic Programs. In Prog. Lang. Design and Impl. (PLDI'18)."},{"key":"e_1_2_2_70_1","volume-title":"Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP'17)","author":"Ngo V. C.","unstructured":"V. C. Ngo , Mario Dehesa-Azuara , M. Fredrikson , and J. Hofmann . 2017 . Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP'17) . V. C. Ngo, Mario Dehesa-Azuara, M. Fredrikson, and J. Hofmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP'17)."},{"key":"e_1_2_2_71_1","doi-asserted-by":"crossref","unstructured":"T. Nipkow. 2015. Amortized Complexity Verified. In Interactive Theorem Proving (ITP'15).  T. Nipkow. 2015. Amortized Complexity Verified. In Interactive Theorem Proving (ITP'15).","DOI":"10.1007\/978-3-319-22102-1_21"},{"key":"e_1_2_2_72_1","volume-title":"Badger: Complexity Analysis with Fuzzing and Symbolic Execution. In Int. Symp. on Softw. Testing and Analysis (ISSTA'18)","author":"Noller Y.","unstructured":"Y. Noller , R. Kersten , and C. S. P\u0103s\u0103reanu . 2018 . Badger: Complexity Analysis with Fuzzing and Symbolic Execution. In Int. Symp. on Softw. Testing and Analysis (ISSTA'18) . Y. Noller, R. Kersten, and C. S. P\u0103s\u0103reanu. 2018. Badger: Complexity Analysis with Fuzzing and Symbolic Execution. In Int. Symp. on Softw. Testing and Analysis (ISSTA'18)."},{"key":"e_1_2_2_73_1","doi-asserted-by":"crossref","unstructured":"L. Noschinski F. Emmes and J. Giesl. 2013. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Automated Reasoning 51 ( June 2013 ). Issue 1.  L. Noschinski F. Emmes and J. Giesl. 2013. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Automated Reasoning 51 ( June 2013 ). Issue 1.","DOI":"10.1007\/s10817-013-9277-6"},{"key":"e_1_2_2_74_1","doi-asserted-by":"crossref","unstructured":"F. Olmedo B. L. Kaminski J.-P. Katoen and C. Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Logic in Computer Science (LICS'16).  F. Olmedo B. L. Kaminski J.-P. Katoen and C. Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In Logic in Computer Science (LICS'16).","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_2_75_1","doi-asserted-by":"crossref","unstructured":"G. D. Plotkin. 1977. LCF Considered as a Programming Language. Theor. Comput. Sci. 5 ( 1977 ) 223-255.  G. D. Plotkin. 1977. LCF Considered as a Programming Language. Theor. Comput. Sci. 5 ( 1977 ) 223-255.","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_2_76_1","doi-asserted-by":"crossref","unstructured":"I. Radicek G. Barthe M. Gaboardi D. Garg and F. Zuleger. 2018. Monadic Refinements for Relational Cost Analysis. In Princ. of Prog. Lang. (POPL'18).  I. Radicek G. Barthe M. Gaboardi D. Garg and F. Zuleger. 2018. Monadic Refinements for Relational Cost Analysis. In Princ. of Prog. Lang. (POPL'18).","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_77_1","doi-asserted-by":"crossref","unstructured":"G. Ramalingam. 1996. Data Flow Frequency Analysis. In Prog. Lang. Design and Impl. (PLDI'96).  G. Ramalingam. 1996. Data Flow Frequency Analysis. In Prog. Lang. Design and Impl. (PLDI'96).","DOI":"10.1145\/231379.231433"},{"key":"e_1_2_2_78_1","volume-title":"Distance Makes the Types Grow Stronger: A Calculus for Diferential Privacy. In Int. Conf. on Functional Programming (ICFP'10)","author":"Reed J.","unstructured":"J. Reed and B. C. Pierce . 2010 . Distance Makes the Types Grow Stronger: A Calculus for Diferential Privacy. In Int. Conf. on Functional Programming (ICFP'10) . J. Reed and B. C. Pierce. 2010. Distance Makes the Types Grow Stronger: A Calculus for Diferential Privacy. In Int. Conf. on Functional Programming (ICFP'10)."},{"key":"e_1_2_2_79_1","doi-asserted-by":"crossref","unstructured":"F. A. Saad C. E. Freer M. C. Rinard and V. K. Mansinghka. 2020. Optimal Approximate Sampling from Discrete Probability Distributions. In Princ. of Prog. Lang. (POPL'20).  F. A. Saad C. E. Freer M. C. Rinard and V. K. Mansinghka. 2020. Optimal Approximate Sampling from Discrete Probability Distributions. In Princ. of Prog. Lang. (POPL'20).","DOI":"10.1145\/3371104"},{"key":"e_1_2_2_80_1","doi-asserted-by":"crossref","unstructured":"M. Sinn F. Zuleger and H. Veith. 2014. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verif. (CAV'14).  M. Sinn F. Zuleger and H. Veith. 2014. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verif. (CAV'14).","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_2_81_1","series-title":"SIAM J. Algebraic Discrete Methods 6 (","volume-title":"Amortized Computational Complexity","author":"Tarjan R. E.","year":"1985","unstructured":"R. E. Tarjan . 1985. Amortized Computational Complexity . SIAM J. Algebraic Discrete Methods 6 ( August 1985 ). Issue 2. R. E. Tarjan. 1985. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods 6 ( August 1985 ). Issue 2."},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_2_2_84_1","doi-asserted-by":"crossref","unstructured":"Andre W Visser. 1997. Using random walk models to simulate the vertical distribution of particles in a turbulent water column. Marine Ecology Progress Series 158 ( 1997 ) 275-281.  Andre W Visser. 1997. Using random walk models to simulate the vertical distribution of particles in a turbulent water column. Marine Ecology Progress Series 158 ( 1997 ) 275-281.","DOI":"10.3354\/meps158275"},{"key":"e_1_2_2_85_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker D.","unstructured":"D. Walker . 2002. Substructural Type Systems . In Advanced Topics in Types and Programming Languages . MIT Press . D. Walker. 2002. Substructural Type Systems. In Advanced Topics in Types and Programming Languages. MIT Press."},{"key":"e_1_2_2_86_1","doi-asserted-by":"crossref","unstructured":"D. Wang and J. Hofmann. 2019. Type-Guided Worst-Case Input Generation. In Princ. of Prog. Lang. (POPL'19).  D. Wang and J. Hofmann. 2019. Type-Guided Worst-Case Input Generation. In Princ. of Prog. Lang. (POPL'19).","DOI":"10.1145\/3290326"},{"key":"e_1_2_2_87_1","volume-title":"Tail Bound Analysis for Probabilistic Programs via Central Moments. arXiv","author":"Wang Di","year":"2001","unstructured":"Di Wang , Jan Hofmann , and Thomas Reps . 2020a. Tail Bound Analysis for Probabilistic Programs via Central Moments. arXiv : 2001 . 10150 [cs.PL] Di Wang, Jan Hofmann, and Thomas Reps. 2020a. Tail Bound Analysis for Probabilistic Programs via Central Moments. arXiv: 2001. 10150 [cs.PL]"},{"key":"e_1_2_2_88_1","volume-title":"Raising Expectations: Automating Expected Cost Analysis with Types. arXiv","author":"Wang Di","year":"2020","unstructured":"Di Wang , David M Kahn , and Jan Hofmann . 2020 b. Raising Expectations: Automating Expected Cost Analysis with Types. arXiv : 2006. 14010 [cs.PL] Di Wang, David M Kahn, and Jan Hofmann. 2020b. Raising Expectations: Automating Expected Cost Analysis with Types. arXiv: 2006. 14010 [cs.PL]"},{"key":"e_1_2_2_89_1","doi-asserted-by":"crossref","unstructured":"P. Wang H. Fu A. K. Goharshady K. Chatterjee X. Qin and W. Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. In Prog. Lang. Design and Impl. (PLDI'19).  P. Wang H. Fu A. K. Goharshady K. Chatterjee X. Qin and W. Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. In Prog. Lang. Design and Impl. (PLDI'19).","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_2_2_90_1","doi-asserted-by":"crossref","unstructured":"P. Wang D. Wang and A. Chlipala. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. In Object-Oriented Prog. Syst. Lang. and Applications (OOPSLA'17).  P. Wang D. Wang and A. Chlipala. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. In Object-Oriented Prog. Syst. Lang. and Applications (OOPSLA'17).","DOI":"10.1145\/3133903"},{"key":"e_1_2_2_91_1","volume-title":"Probability with Martingales","author":"Williams D.","unstructured":"D. Williams . 1991. Probability with Martingales . Cambridge University Press . D. Williams. 1991. Probability with Martingales. Cambridge University Press."},{"key":"e_1_2_2_92_1","unstructured":"D. Wingate and T. Weber. 2013. Automated Variational Inference in Probabilistic Programming. Technical Report. Computing Research Repository.  D. Wingate and T. Weber. 2013. Automated Variational Inference in Probabilistic Programming. Technical Report. Computing Research Repository."},{"key":"e_1_2_2_93_1","doi-asserted-by":"crossref","unstructured":"H. Xi. 2002. Dependent Types for Program Termination Verification. J. Higher-Order and Symbolic Comp. 15 ( 2002 ). Issue 1.  H. Xi. 2002. Dependent Types for Program Termination Verification. J. Higher-Order and Symbolic Comp. 15 ( 2002 ). Issue 1.","DOI":"10.1023\/A:1019916231463"},{"key":"e_1_2_2_94_1","volume-title":"Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS'11)","author":"Zuleger F.","unstructured":"F. Zuleger , M. Sinn , S. Gulwani , and H. Veith . 2011 . Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS'11) . F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. 2011. Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS'11)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408992","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408992","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408992","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:59Z","timestamp":1750178879000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408992"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":93,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408992"],"URL":"https:\/\/doi.org\/10.1145\/3408992","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}