{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:35Z","timestamp":1775790815567,"version":"3.50.1"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"the United States Air Force under DARPA AA Contract","award":["FA8750-18-C-0092"],"award-info":[{"award-number":["FA8750-18-C-0092"]}]},{"name":"SHF","award":["1812876"],"award-info":[{"award-number":["1812876"]}]},{"name":"the National Science Foundation under SaTC","award":["1801369"],"award-info":[{"award-number":["1801369"]}]},{"name":"the United States Air Force under DARPA STAC Contract","award":["FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-15-C-0082"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>This paper presents a novel technique for type-guided worst-case input generation for functional programs. The technique builds on automatic amortized resource analysis (AARA), a type-based technique for deriving symbolic bounds on the resource usage of functions. Worst-case input generation is performed by an algorithm that takes as input a function, its resource-annotated type derivation in AARA, and a skeleton that describes the shape and size of the input that is to be generated. If successful, the algorithm fills in integers, booleans, and data structures to produce a value of the shape given by the skeleton. The soundness theorem states that the generated value exhibits the highest cost among all arguments of the functions that have the shape of the skeleton. This cost corresponds exactly to the worst-case bound that is established by the type derivation. In this way, a successful completion of the algorithm proves that the bound is tight for inputs of the given shape. Correspondingly, a relative completeness theorem is proved to show that the algorithm succeeds if and only if the derived worst-case bound is tight. The theorem is relative because it depends on a decision procedure for constraint solving. The technical development is presented for a simple first-order language with linear resource bounds. However, the technique scales to and has been implemented for Resource Aware ML, an implementation of AARA for a fragment of OCaml with higher-order functions, user-defined data types, and types for polynomial bounds. Experiments demonstrate that the technique works effectively and can derive worst-case inputs with hundreds of integers for sorting algorithms, operations on search trees, and insertions into hash tables.<\/jats:p>","DOI":"10.1145\/3290326","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Type-guided worst-case input generation"],"prefix":"10.1145","volume":"3","author":[{"given":"Di","family":"Wang","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_6"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_2_2_5_1","volume-title":"Int. Conf. on Rewriting Techniques and Applications (RTA\u201913)","author":"Avanzini M.","unstructured":"M. Avanzini and G. Moser . 2013. A Combination Framework for Complexity . In Int. Conf. on Rewriting Techniques and Applications (RTA\u201913) . M. Avanzini and G. Moser. 2013. A Combination Framework for Complexity. In Int. Conf. on Rewriting Techniques and Applications (RTA\u201913)."},{"key":"e_1_2_2_6_1","volume-title":"ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning (LPAR\u201910).","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\u201910). 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\u201910)."},{"key":"e_1_2_2_7_1","volume":"201","author":"Brockschmidt M.","unstructured":"M. Brockschmidt , F. Emmes , S. Falke , C. Fuhs , and J. Giesl. 201 4. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201914). 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\u201914).","journal-title":"J. Giesl."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070545"},{"key":"e_1_2_2_9_1","volume-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Op. Syst. Design and Impl. (OSDI\u201908).","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Op. Syst. Design and Impl. (OSDI\u201908). C. Cadar, D. Dunbar, and D. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Op. Syst. Design and Impl. (OSDI\u201908)."},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Q. Carbonneaux J. Hoffmann T. Reps and Z. Shao. 2017. Automated Resource Analysis with Coq Proof Objects. In Computer Aided Verif. (CAV\u201917).  Q. Carbonneaux J. Hoffmann T. Reps and Z. Shao. 2017. Automated Resource Analysis with Coq Proof Objects. In Computer Aided Verif. (CAV\u201917).","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542517"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"A. Chargu\u00e9raud and F. Pottier. 2015. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In Interactive Theorem Proving (ITP\u201915).  A. Chargu\u00e9raud and F. Pottier. 2015. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In Interactive Theorem Proving (ITP\u201915).","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2110356.2110358"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_2_16_1","volume-title":"Refinement Types for Incremental Computational Complexity. In European Symp. on Programming (ESOP\u201915)","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\u201915) . E. \u00c7i\u00e7ek, D. Garg, and U. A. Acar. 2015. Refinement Types for Incremental Computational Complexity. In European Symp. on Programming (ESOP\u201915)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_2_19_1","volume-title":"USENIX Sec. Symp. (USENIX\u201903)","author":"Crosby S. A.","unstructured":"S. A. Crosby and D. S. Wallach . 2003. Denial of Service via Algorithmic Complexity Attacks . In USENIX Sec. Symp. (USENIX\u201903) . S. A. Crosby and D. S. Wallach. 2003. Denial of Service via Algorithmic Complexity Attacks. In USENIX Sec. Symp. (USENIX\u201903)."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"L. de Moura and N. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201908).   L. de Moura and N. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS\u201908).","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642951"},{"key":"e_1_2_2_24_1","volume-title":"Resource Analysis of Complex Programs with Cost Equations. In Asian Symp. on Prog. Lang. and Systems (APLAS\u201914)","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\u201914) . 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\u201914)."},{"key":"e_1_2_2_25_1","volume-title":"An Empirical Study of the Robustness of Windows NT Applications Using Random Testing. In USENIX Windows Syst. Symp. (WSS\u201900)","author":"Forrester J. E.","unstructured":"J. E. Forrester and B. P. Miller . 2000 . An Empirical Study of the Robustness of Windows NT Applications Using Random Testing. In USENIX Windows Syst. Symp. (WSS\u201900) . J. E. Forrester and B. P. Miller. 2000. An Empirical Study of the Robustness of Windows NT Applications Using Random Testing. In USENIX Windows Syst. Symp. (WSS\u201900)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_37"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_2_28_1","unstructured":"P. Godefroid M. Levin and D. Molnar. 2008. Automated Whitebox Fuzz Testing. In Network and Dist. Syst. Security (NDSS\u201908).  P. Godefroid M. Levin and D. Molnar. 2008. Automated Whitebox Fuzz Testing. In Network and Dist. Syst. Security (NDSS\u201908)."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_2_2_31_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_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_2_34_1","volume-title":"Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP\u201910)","author":"Hoffmann J.","unstructured":"J. Hoffmann and M. Hofmann . 2010 . Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP\u201910) . J. Hoffmann and M. Hofmann. 2010. Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP\u201910)."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_2_36_1","volume-title":"Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA\u201915)","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\u201915) . M. Hofmann and G. Moser. 2015. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA\u201915)."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"U. D. Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS\u201911).  U. D. Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS\u201911).","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_2_2_43_1","volume-title":"Symbolic Complexity Analysis Using Context-Preserving Histories. In Int. Conf. on Softw. Testing, Verif. and Validation (ICST\u201917)","author":"Luckow K.","unstructured":"K. Luckow , R. Kersten , and C. P\u0103s\u0103reanu . 2017 . Symbolic Complexity Analysis Using Context-Preserving Histories. In Int. Conf. on Softw. Testing, Verif. and Validation (ICST\u201917) . K. Luckow, R. Kersten, and C. P\u0103s\u0103reanu. 2017. Symbolic Complexity Analysis Using Context-Preserving Histories. In Int. Conf. on Softw. Testing, Verif. and Validation (ICST\u201917)."},{"key":"e_1_2_2_44_1","volume-title":"Static Analysis Symp. (SAS\u201911)","author":"Ma K.-K.","unstructured":"K.-K. Ma , K. Y. Phang , J. S. Foster , and M. Hicks . 2011. Directed symbolic execution . In Static Analysis Symp. (SAS\u201911) . K.-K. Ma, K. Y. Phang, J. S. Foster, and M. Hicks. 2011. Directed symbolic execution. In Static Analysis Symp. (SAS\u201911)."},{"key":"e_1_2_2_45_1","volume-title":"A Killer Adversary for Quicksort. J. Softw.-Practice &amp","author":"McIlroy M. D.","year":"1999","unstructured":"M. D. McIlroy . 1999. A Killer Adversary for Quicksort. J. Softw.-Practice &amp ; Experience 29 ( April 1999 ). Issue 4. M. D. McIlroy. 1999. A Killer Adversary for Quicksort. J. Softw.-Practice &amp; Experience 29 (April 1999). Issue 4."},{"key":"e_1_2_2_46_1","volume":"201","author":"Ngo V. C.","unstructured":"V. C. Ngo , Mario Dehesa-Azuara , M. Fredrikson , and J. Hoffmann. 201 7. Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP\u201917). V. C. Ngo, Mario Dehesa-Azuara, M. Fredrikson, and J. Hoffmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP\u201917).","journal-title":"J. Hoffmann."},{"key":"e_1_2_2_47_1","doi-asserted-by":"crossref","unstructured":"T. Nipkow. 2015. Amortized Complexity Verified. In Interactive Theorem Proving (ITP\u201915).  T. Nipkow. 2015. Amortized Complexity Verified. In Interactive Theorem Proving (ITP\u201915).","DOI":"10.1007\/978-3-319-22102-1_21"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213868"},{"key":"e_1_2_2_49_1","volume":"201","author":"Noschinski L.","unstructured":"L. Noschinski , F. Emmes , and J. Giesl. 201 3. 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.","journal-title":"J. Giesl."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134073"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364575"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_2_55_1","series-title":"SIAM J. Algebraic Discrete Methods 6 (August","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_57_1","volume-title":"Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In European Symp. on Programming (ESOP\u201915)","author":"Vasconcelos P. B.","unstructured":"P. B. Vasconcelos , S. Jost , M. Florido , and K. Hammond . 2015 . Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In European Symp. on Programming (ESOP\u201915) . P. B. Vasconcelos, S. Jost, M. Florido, and K. Hammond. 2015. Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In European Symp. on Programming (ESOP\u201915)."},{"key":"e_1_2_2_58_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_59_1","volume":"201","author":"Wang D.","unstructured":"D. Wang and J. Hoffmann. 201 8. Type-Guided Worst-Case Input Generation. Available on https:\/\/www.cs.cmu.edu\/~diw3\/ papers\/WangH18.pdf . D. Wang and J. Hoffmann. 2018. Type-Guided Worst-Case Input Generation. Available on https:\/\/www.cs.cmu.edu\/~diw3\/ papers\/WangH18.pdf .","journal-title":"J. Hoffmann."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"e_1_2_2_61_1","first-page":"2011","volume":"201","unstructured":"Website. 201 1. CVE - CVE- 2011 - 4885 . Available on: https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2011- 4885 . Website. 2011. CVE - CVE-2011-4885. Available on: https:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi?name=CVE- 2011- 4885 .","journal-title":"Website."},{"key":"e_1_2_2_62_1","unstructured":"Website. 2012a. PHP 5.3.8 - Hashtables Denial of Service. Available on https:\/\/www.exploit- db.com\/exploits\/18296\/ .  Website. 2012a. PHP 5.3.8 - Hashtables Denial of Service. Available on https:\/\/www.exploit- db.com\/exploits\/18296\/ ."},{"key":"e_1_2_2_63_1","volume-title":"PHP: PHP 5 ChangeLog. Available on http:\/\/www.php.net\/ChangeLog- 5.php#5.3.9 .","year":"2012","unstructured":"Website. 2012 b. PHP: PHP 5 ChangeLog. Available on http:\/\/www.php.net\/ChangeLog- 5.php#5.3.9 . Website. 2012b. PHP: PHP 5 ChangeLog. Available on http:\/\/www.php.net\/ChangeLog- 5.php#5.3.9 ."},{"key":"e_1_2_2_64_1","unstructured":"Website. 2015. Space\/Time Analysis for Cybersecurity (STAC). Available on https:\/\/www.darpa.mil\/program\/ space- time- analysis- for- cybersecurity .  Website. 2015. Space\/Time Analysis for Cybersecurity (STAC). Available on https:\/\/www.darpa.mil\/program\/ space- time- analysis- for- cybersecurity ."},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"},{"key":"e_1_2_2_66_1","volume-title":"Regular Property Guided Dynamic Symbolic Execution. In Int. Conf. on Softw. Eng. (ICSE\u201915)","author":"Zhang Y.","unstructured":"Y. Zhang , Z. Chen , J. Wang , W. Dong , and Z. Liu . 2015 . Regular Property Guided Dynamic Symbolic Execution. In Int. Conf. on Softw. Eng. (ICSE\u201915) . Y. Zhang, Z. Chen, J. Wang, W. Dong, and Z. Liu. 2015. Regular Property Guided Dynamic Symbolic Execution. In Int. Conf. on Softw. Eng. (ICSE\u201915)."},{"key":"e_1_2_2_67_1","volume-title":"Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS\u201911)","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\u201911) . 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\u201911)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290326","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":66,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290326"],"URL":"https:\/\/doi.org\/10.1145\/3290326","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}