{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T03:21:15Z","timestamp":1762917675341,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296036"},{"type":"electronic","value":"9783319296043"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29604-3_10","type":"book-chapter","created":{"date-parts":[[2016,2,20]],"date-time":"2016-02-20T07:53:12Z","timestamp":1455954792000},"page":"144-162","source":"Crossref","is-referenced-by-count":10,"title":["A Coq Library for Internal Verification of Running-Times"],"prefix":"10.1007","author":[{"given":"Jay","family":"McCarthy","sequence":"first","affiliation":[]},{"given":"Burke","family":"Fetscher","sequence":"additional","affiliation":[]},{"given":"Max","family":"New","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Feltey","sequence":"additional","affiliation":[]},{"given":"Robert Bruce","family":"Findler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,21]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-3-642-12032-9_21","volume-title":"Foundations of Software Science and Computational Structures","author":"Thorsten Altenkirch","year":"2010","unstructured":"Altenkirch, T., Chapman, J., Uustalu, T.: Monads need not be endofunctors. In: Proceedings of the Foundations of Software Science and Computation Structure (2010)"},{"issue":"3\u20134","key":"10_CR2","first-page":"335","volume":"19","author":"R Atkey","year":"2009","unstructured":"Atkey, R.: Parameterised notions of computation. JFP 19(3\u20134), 335\u2013376 (2009)","journal-title":"JFP"},{"key":"10_CR3","unstructured":"Braun, W., Rem, M.: A logarithmic Implementation of Flexible Arrays. Eindhoven University of Technology, MR83\/4 (1983)"},{"key":"10_CR4","unstructured":"Chargu\u00e9raud, A.: Characteristic Formulae for Mechanized Program Verification. Ph.D. dissertation, Universit\u00e9 Paris Diderot (Paris 7) (2010)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Proceedings of the ITP (2015)","DOI":"10.1007\/978-3-319-22102-1_9"},{"key":"10_CR6","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Proceedings of the POPL (2000)","DOI":"10.1145\/325694.325716"},{"key":"10_CR8","unstructured":"Crosby, S.A., Wallach, D.S.: Denial of service via algorithmic complexity attacks. In: Proceedings of the USENIX Security Symposium (2003)"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Proceedings of the POPL (2008)","DOI":"10.1145\/1328438.1328457"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Danner, N., Paykin, J., Royer, J.S.: A static cost analysis for a higher-order language. In: Proceedings of the Workshop on Programming Languages meets Program Verification (2013)","DOI":"10.1145\/2428116.2428123"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-24725-8_26","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., Letouzey, P.: Functors for proofs and programs. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 370\u2013384. Springer, Heidelberg (2004)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: SPEED: precise and efficient static estimation of program computational complexity. In: Proceedings of the POPL (2009)","DOI":"10.1145\/1480881.1480898"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-662-46669-8_6","volume-title":"Programming Languages and Systems","author":"J Hoffmann","year":"2015","unstructured":"Hoffmann, J., Shao, Z.: Automatic static cost analysis for parallel programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 132\u2013157. Springer, Heidelberg (2015)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proceedings of the POPL (2003)","DOI":"10.1145\/604131.604148"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L.: Recursion and Dynamic Data-structures in bounded space: towards embedded ML programming. In: Proceedings of the ICFP (1999)","DOI":"10.1145\/317636.317785"},{"issue":"6","key":"10_CR16","first-page":"661","volume":"7","author":"C Okasaki","year":"1997","unstructured":"Okasaki, C.: Three algorithms on braun trees. JFP 7(6), 661\u2013666 (1997)","journal-title":"JFP"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Rosendahl, M.: Automatic complexity analysis. In: Proceedings of the International Conference on Functional Programming Languages And Computer Architecture (1989)","DOI":"10.1145\/99370.99381"},{"key":"10_CR18","unstructured":"Sozeau, M.: Subset coercions in Coq. In: Proceedings of the TYPES (2006)"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the dijkstra monad. In: Proceedings of the PLDI (2013)","DOI":"10.1145\/2491956.2491978"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Swierstra, W.: A hoare logic for the state monad. In: Proceedings of the TPHOLS (2009)","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-02444-3_16","volume-title":"Types for Proofs and Programs","author":"E Weegen van der","year":"2009","unstructured":"van der Weegen, E., McKinna, J.: A machine-checked proof of the average-case complexity of quicksort in Coq. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 256\u2013271. Springer, Heidelberg (2009)"},{"key":"10_CR22","unstructured":"Xi, H.: Dependently typed data structures. In: Proceedings of the Workshop on Algorithmic Aspects of Advanced Programming Languages (1999a)"},{"key":"10_CR23","unstructured":"Xi, H.: Dependently Types in Practical Programming. Ph.D. dissertation, Carnegie Mellon University (1999b)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependently types in practical programming. In: Proceedings of the POPL (1999)","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29604-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T10:51:03Z","timestamp":1559386263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29604-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296036","9783319296043"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29604-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}