{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:04Z","timestamp":1725663604253},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_59","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:46:17Z","timestamp":1330191977000},"page":"459-474","source":"Crossref","is-referenced-by-count":2,"title":["Complexity of proving program correctness"],"prefix":"10.1007","author":[{"given":"Hardi","family":"Hungar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","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":"22_CR2","unstructured":"Clarke, E. M. The characterization problem for Hoare logic, Rep. CMU-CS-84-109, Carnegie-Mellon Univ. (1984)."},{"key":"22_CR3","doi-asserted-by":"publisher","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":"22_CR4","first-page":"43","volume":"7","author":"R. Fagin","year":"1974","unstructured":"Fagin, R. Generalized first-order spectra and polynomial-time recognizable sets, SIAM-AMS Proc. 7 (1974) 43\u201373.","journal-title":"SIAM-AMS Proc."},{"key":"22_CR5","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":"22_CR6","first-page":"106","volume":"193","author":"A. Goerdt","year":"1985","unstructured":"Goerdt, A. A Hoare calculus defined by recursion on higher types, in: Proc. Logics of Programs 1985, LNCS 193, 106\u2013117.","journal-title":"LNCS"},{"key":"22_CR7","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":"22_CR8","doi-asserted-by":"publisher","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":"22_CR9","doi-asserted-by":"crossref","unstructured":"Hartmanis, J., Immerman, N. and Mahany, S. One-way log-tape reductions, 19th FoCS (1978) 65\u201372.","DOI":"10.1109\/SFCS.1978.31"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Immerman, N. Languages which capture complexity classes, 15th SToC (1983) 347\u2013354.","DOI":"10.1145\/800061.808765"},{"key":"22_CR11","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":"22_CR12","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":"22_CR13","unstructured":"Juszczyk, M. On equivalence between language L4 and recursive definitions of higher types, not published (submitted for MFCS'89) Warsaw (1989)."},{"key":"22_CR14","unstructured":"Kfoury, A. J., Tiuryn, J. and Urzyczyn, P. The hierarchy of finitely typed functions, 2nd LiCS (1987) 225\u2013235."},{"key":"22_CR15","unstructured":"Kfoury, A. J. and Urzyczyn, P. Finitely typed functional programs. Part II: Comparisons to imperative languages, Res. Rep. Boston Univ. (1988)."},{"key":"22_CR16","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":"22_CR17","unstructured":"Olderog, E.-R. charakterisierung Hoarescher Systeme f\u00fcr ALGOL-\u00e4hnliche Programmiersprachen, Dissertation, Univ. Kiel (1981)."},{"key":"22_CR18","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":"22_CR19","doi-asserted-by":"publisher","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","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_59.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:54:15Z","timestamp":1605628455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_59"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_59","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}