{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:34Z","timestamp":1725663634798},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540565031"},{"type":"electronic","value":"9783540475743"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56503-5_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:15:58Z","timestamp":1330254958000},"page":"428-439","source":"Crossref","is-referenced-by-count":1,"title":["The complexity of verifying functional programs"],"prefix":"10.1007","author":[{"given":"Hardi","family":"Hungar","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"43_CR1","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E. M. Clarke","year":"1979","unstructured":"Clarke, E. M., Programming languages for which it is impossible to obtain good Hoare axiom systems, JACM 26 (1979) 129\u2013147.","journal-title":"JACM"},{"key":"43_CR2","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S. A. Cook","year":"1978","unstructured":"Cook, S. A., Soundness and completeness of an axiom system for program verification, SIAM J. Comp. 7 (1978) 70\u201390.","journal-title":"SIAM J. Comp."},{"key":"43_CR3","doi-asserted-by":"crossref","first-page":"612","DOI":"10.1145\/2402.322394","volume":"30","author":"E. M. Clarke","year":"1983","unstructured":"Clarke, E. M., German, S. M. and Halpern, J. Y., Effective axiomatizations of Hoare logics, JACM 30 (1983) 612\u2013636.","journal-title":"JACM"},{"key":"43_CR4","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0890-5401(89)90040-0","volume":"83","author":"S. M. German","year":"1989","unstructured":"German, S. M., Clarke, E. M. and Halpern, J. Y., Reasoning about procedures as parameters in the language L4, Inf. and Comp. 83 (1989) 265\u2013359. (Earlier version: 1st LiCS (1986) 11\u201325)","journal-title":"Inf. and Comp."},{"key":"43_CR5","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/3-540-15648-8_9","volume":"193","author":"A. Goerdt","year":"1985","unstructured":"Goerdt, A., A Hoare calculus for functions defined by recursion on higher types, In: Proc. Logics of Programs 1985, LNCS 193, 106\u2013117.","journal-title":"Proc. Logics of Programs"},{"key":"43_CR6","first-page":"329","volume":"324","author":"A. Goerdt","year":"1988","unstructured":"Goerdt, A., Hoare calculi for higher type control structures and their completeness in the sense of Cook, MFCS 88, LNCS 324 (1988) 329\u2013338.","journal-title":"MFCS 88, LNCS"},{"key":"43_CR7","unstructured":"Goerdt, A. Hoare logic for lambda-terms as basis of Hoare logic for imperative languages, Proc. 2nd LiCS (1987) 293\u2013299."},{"key":"43_CR8","unstructured":"Goerdt, A. Characterizing complexity classes by general recursive definitions in higher types, in: E. B\u00f6rger and H. Kleine-B\u00fcning, CSL '88, Proceedings, LNCS 385 (1988)."},{"key":"43_CR9","doi-asserted-by":"crossref","unstructured":"Grabowski, M. und Hungar, H. On the existence of effective Hoare logics, Proc. 3rd LiCS (1988) 428\u2013435.","DOI":"10.1109\/LICS.1988.5140"},{"key":"43_CR10","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/S0019-9958(84)80023-6","volume":"60","author":"D. Harel","year":"1984","unstructured":"Harel, D. and Peleg, D., On static logics, dynamic logics, and complexity classes, Inf. and Contr. 60 (1984) 86\u2013102.","journal-title":"Inf. and Contr."},{"key":"43_CR11","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1007\/3-540-54415-1_59","volume":"526","author":"H. Hungar","year":"1991","unstructured":"Hungar, H., Complexity of proving program correctness, Proc. Theoretical Aspects of Computer Software 1991, LNCS 526, 459\u2013474.","journal-title":"Proc. Theoretical Aspects of Computer Software"},{"key":"43_CR12","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1145\/322003.322016","volume":"24","author":"N. D. Jones","year":"1977","unstructured":"Jones, N. D. and Muchnik, S. S., Even simple programs are hard to analyze, JACM 24 (1977) 338\u2013350.","journal-title":"JACM"},{"key":"43_CR13","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/322063.322074","volume":"25","author":"N. D. Jones","year":"1978","unstructured":"Jones, N. D. and Muchnik, S. S., The complexity of finite memory programs with recursion, JACM 25 (1978) 312\u2013321.","journal-title":"JACM"},{"key":"43_CR14","unstructured":"Kfoury, A. J., Tiuryn, J. and Urzyczyn, P. The hierarchie of finitely typed functions, 2nd LiCS (1987) 225\u2013235."},{"key":"43_CR15","first-page":"110","volume":"2","author":"H. Langmaack","year":"1973","unstructured":"Langmaack, H., On correct procedure parameter transmission in higher programming languages, Acta Inf. 2 (1973) 110\u2013142.","journal-title":"Acta Inf."},{"key":"43_CR16","doi-asserted-by":"crossref","unstructured":"Olderog, E.-R. A characterization of Hoare's logic for programs with PASCAL-like procedures, 15th SToC (1983) 320\u2013329.","DOI":"10.1145\/800061.808761"},{"key":"43_CR17","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. D. Plotkin","year":"1977","unstructured":"Plotkin, G. D., LCF considered as a programming language, TCS 5 (1977) 223\u2013255.","journal-title":"TCS"},{"key":"43_CR18","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(88)90052-7","volume":"60","author":"J. Tiuryn","year":"1988","unstructured":"Tiuryn, J. and Urzyczyn, P., Some relationships between logics of programs and complexity theory, TCS 60 (1988) 83\u2013108. (Earlier version: 24th FoCS (1983) 180\u2013184)","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","STACS 93"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56503-5_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:04:22Z","timestamp":1605647062000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56503-5_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540565031","9783540475743"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-56503-5_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}