{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T22:22:45Z","timestamp":1779315765710,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540156482","type":"print"},{"value":"9783540395270","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_9","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:22:30Z","timestamp":1330176150000},"page":"106-117","source":"Crossref","is-referenced-by-count":5,"title":["A Hoare Calculus for functions defined by recursion on higher types"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Goerdt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E.M. Clarke","year":"1979","unstructured":"E.M. Clarke, Programming language constructs for which it is impossible to obtain good Hoare \u2014 like axioms, JACM 26, 129\u2013147, (1979)","journal-title":"JACM"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, S.M. German, J.Y. Halpern, On effective axiomatizations of Hoare logics, Proceedings 9th POPL, 309\u2013321, (1982)","DOI":"10.1145\/582153.582186"},{"key":"9_CR3","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF00264295","volume":"20","author":"W. Damm","year":"1983","unstructured":"W. Damm, B. Josko, A sound and relatively* complete Hoare-Logic for a language with higher type procedures, Acta Informatica 20, 59\u2013101, (1983)","journal-title":"Acta Informatica"},{"key":"9_CR4","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1007\/BFb0025776","volume":"134","author":"J.W. deBakker","year":"1982","unstructured":"J.W. deBakker, J.-J.Ch. Meyer, J.W. Klop, Correctness of programs with function procedures, Proceedings Logics of programs, LNCS 134, 94\u2013112, (1982)","journal-title":"Proceedings Logics of programs, LNCS"},{"key":"9_CR5","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF00264436","volume":"18","author":"G.W. Ernst","year":"1982","unstructured":"G.W. Ernst, J.K. Navlakha, W.F. Ogden, Verification of programs with procedure type parameters, Acta Informatica 18, 149\u2013169, (1982)","journal-title":"Acta Informatica"},{"key":"9_CR6","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/3-540-12896-4_365","volume":"164","author":"S.M. German","year":"1983","unstructured":"S.M. German, E.M. Clarke, J.Y. Halpern, Reasoning about procedures as parameters, Proceedings Logics of programs, LNCS 164, 206\u2013220, (1983)","journal-title":"Proceedings Logics of programs, LNCS"},{"key":"9_CR7","unstructured":"A. Goerdt, Ein Hoare Kalk\u00fcl f\u00fcr getypte \u03bb-Terme \u2014 Korrektheit, Vollst\u00e4ndigkeit, Anwendungen, RWTH Aachen"},{"key":"9_CR8","first-page":"73","volume":"166","author":"B. Josko","year":"1984","unstructured":"B. Josko, On expressive interpretations of a Hoare-logic for Clarke's language L 4, STACS 1984, LNCS 166, 73\u201384, (1984)","journal-title":"LNCS"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"A. Kanda, Effektive solutions of recursive domain equations, Thesis Warwick, (1979)","DOI":"10.1007\/3-540-09526-8_30"},{"key":"9_CR10","first-page":"241","volume":"158","author":"H. Langmaack","year":"1983","unstructured":"H. Langmaack, Aspects of programs with finite modes, FCT 83, LNCS 158, 241\u2013254, (1983)","journal-title":"FCT 83, LNCS"},{"key":"9_CR11","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0304-3975(84)90066-5","volume":"30","author":"E.-R. Olderog","year":"1984","unstructured":"E.-R. Olderog, Correctness of programs with PASCAL \u2014 like procedures without global variables, TCS 30, 49\u201390, (1984)","journal-title":"TCS"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"M. Sintzoff, Proof \u2014 oriented and applicative valuations in definitions of algorithms, Proceedings of the 1981 Conference on Functional Programming Languages and Computer Architecture, 155\u2013162, (1981)","DOI":"10.1145\/800223.806774"},{"key":"9_CR13","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1016\/S0019-9958(83)80006-0","volume":"56","author":"P. Urzyczyn","year":"1983","unstructured":"P. Urzyczyn, A necessary and sufficient condition in order that a Herbrand interpretation is expressive relative to recursive programs, Information and Control 56, 212\u2013219, (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:08:38Z","timestamp":1605625718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1985]]}}}