{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:33Z","timestamp":1725663333438},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540128960"},{"type":"electronic","value":"9783540387756"}],"license":[{"start":{"date-parts":[[1984,1,1]],"date-time":"1984-01-01T00:00:00Z","timestamp":441763200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1984]]},"DOI":"10.1007\/3-540-12896-4_362","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T12:56:53Z","timestamp":1330174613000},"page":"161-175","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A sound and relatively complete axiomatization of clarke's language L4"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"Josko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/321992.321997","volume":"24","author":"J. A. Goguen","year":"1977","unstructured":"Goguen, J.A.\/Thatcher, J.W.\/Wagner, E.G.\/Wright, J.B.: Initial algebra semantics and continuous algebras. J.ACM 24, 68\u201395 (1977)","journal-title":"J.ACM"},{"key":"12_CR2","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. R. Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare's logic: a survey-part I. ACM TOPLAS 3, 431\u2013483 (1981)","journal-title":"ACM TOPLAS"},{"key":"12_CR3","series-title":"Report IW","volume-title":"Correctness of programs with function procedures","author":"J. W. Bakker de","year":"1981","unstructured":"de Bakker, J.W.\/Klop, J.W.\/Meyer J.-J.Ch.: Correctness of programs with function procedures. Report IW 170\/81, Mathematisch Centrum, Amsterdam (1981)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P.: The type free lambda calculus. Handbook of Mathematical Logic, North-Holland (1977)","DOI":"10.1016\/S0049-237X(08)71129-7"},{"key":"12_CR5","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 language constructs for which it is impossible to obtain good Hoare-like axioms. JACM 26, 129\u2013147 (1979)","journal-title":"JACM"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M.,\/German, S.M.\/Halpern, J.Y.: On effective axiomatizations of Hoare-logics. 9th Anual ACM Symposium on Principles of Programming Languages, 309\u2013321 (1982)","DOI":"10.1145\/582153.582186"},{"key":"12_CR7","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. Comput. 7, 70\u201390 (1978)","journal-title":"SIAM J. Comput."},{"key":"12_CR8","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(82)90009-3","volume":"20","author":"W. Damm","year":"1982","unstructured":"Damm, W.: The IO \u2014 and OI \u2014 hierarchies. TCS 20, 95\u2013207 (1982)","journal-title":"TCS"},{"key":"12_CR9","unstructured":"Damm, W.\/Fehr, E.: A schematological approach to the analysis of the procedure concept in ALGOL-languages. Proc. 5\u00e8me Colloque sur les Arbres en Alg\u00e8bre et en Programmation, Lille, 130\u2013134 (1980)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Damm, W.\/Josko, B.: A sound and relatively* complete Hoare logic for a language with higher type procedures Schriften zur Informatik und Angewandten Mathematik Nr. 77 TH Aachen (1982) (to appear in Acta Informatica)","DOI":"10.1007\/BF00264295"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"German, S.M.\/Clarke, E.M.\/Halpern, J.Y.: A stronger axiom system for reasoning about procedures as parameters. Proc. Workshop on Logics of Programs, Pittsburgh (1983)","DOI":"10.1007\/3-540-12896-4_365"},{"key":"12_CR12","unstructured":"Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and non-recursive programs. Techn. Rep. 75, Dept. of Computer Sci., Univ. of Toronto (1975)"},{"key":"12_CR13","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. R. Hoare","year":"1969","unstructured":"Hoare, C.A. R.: An axiomatic basis for computer programming. Comm. ACM 12 576\u2013583 (1969)","journal-title":"Comm. ACM"},{"key":"12_CR14","unstructured":"Josko, B.: On expressive interpretations of a Hoare-logic for a language with higher type procedures, Schriften zur Informatik und Angewandten Mathematik, Nr. 88,TH Aachen (1983)"},{"key":"12_CR15","unstructured":"Josko, B.: A Hoare-calculus for ALGOL-like programs with finite mode procedures without global variables, Aachen (1983)"},{"key":"12_CR16","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF00289503","volume":"2","author":"H. Langmaack","year":"1973","unstructured":"Langmaack, H.: On procedures as open subroutines I, II Acta Informatica 2, 311\u2013333 (1973) and 3, 227\u2013241 (1974)","journal-title":"Acta Informatica"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Langmaack, H.: On a theory of decision problems in programing languages. Proc. Int. Conf. on Mathematical Studies of Information Processing, LNCS 75, 538\u2013558 (1979)","DOI":"10.1007\/3-540-09541-1_38"},{"key":"12_CR18","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00625282","volume":"18","author":"H. Langmaack","year":"1982","unstructured":"Langmaack, H.: On termination problem for finitely interpreted ALGOL-like programs. Acta Informatica 18, 79\u2013108 (1982)","journal-title":"Acta Informatica"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Langmaack, H.: Aspects of Programs with Finite Modes, Proc. of the International Conference on Foundations of Computation Theory 1983","DOI":"10.1007\/3-540-12689-9_108"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Langmaack, H.\/Olderog, E.-R.: Present-day Hoare-like systems for programming languages with procedures: power limits and most likely extensions. Proc. 7th Coll. Automata, Languages and Programming, LNCS 85, 363\u2013373 (1980)","DOI":"10.1007\/3-540-10003-2_84"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Lipton, R.J.: A nexessary and sufficient condition for the existence of Hoare logics. 18th IEEE Symp. on Foundations of Computer Science, 1\u20136 (1977)","DOI":"10.1109\/SFCS.1977.1"},{"key":"12_CR22","first-page":"161","volume":"16","author":"E.-R. Olderog","year":"1981","unstructured":"Olderog, E.-R.: Sound and complete Hoare-like calculi based on copy rules. Acta Informatica 16, 161\u2013197 (1981)","journal-title":"Acta Informatica"},{"key":"12_CR23","first-page":"65","volume":"50","author":"E. R. Olderog","year":"1981","unstructured":"Olderog, E.R.: Hoare-style proof and formal computations. GI-11. Jahrestagung, IFB 50, 65\u201371 (1981)","journal-title":"GI-11. Jahrestagung, IFB"},{"key":"12_CR24","unstructured":"Olderog, E.-R.: Correctness of programs with PASCAL-like procedures without global variables. (to appear in TCS)"},{"key":"12_CR25","unstructured":"Trakthenbrot, B.A.\/Halpern, J.Y.\/Meyer, A.R.: From denotational to copyrule to axiomatic semantics Proc. Workshop on Logics of Programs, Pittsburgh (1983)."}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-12896-4_362","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:31:12Z","timestamp":1578508272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-12896-4_362"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9783540128960","9783540387756"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-12896-4_362","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1984]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}