{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:21:50Z","timestamp":1725456110144},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540112129"},{"type":"electronic","value":"9783540390473"}],"license":[{"start":{"date-parts":[[1982,1,1]],"date-time":"1982-01-01T00:00:00Z","timestamp":378691200000},"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":[[1982]]},"DOI":"10.1007\/bfb0025776","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T05:23:41Z","timestamp":1132377821000},"page":"94-112","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Correctness of programs with function procedures"],"prefix":"10.1007","author":[{"given":"J. W.","family":"de Bakker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. W.","family":"Klop","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.-J.Ch.","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"unstructured":"APT, K.R., Ten years of Hoare's logic, a survey, in Proc. 5th Scandinavian Logic Symposium (F.V. Jensen, B.H. Mayoh, K.K. M\u00f8ller, eds.), pp 1\u201344, Aalborg University Press, 1979 (revised version to appear in ACM TOPLAS).","key":"7_CR1"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BF00288660","volume":"6","author":"E.A. Ashcroft","year":"1976","unstructured":"ASHCROFT, E.A., M. CLINT & C.A.R. HOARE, Remarks on program proving: jumps and functions, Acta Informatica, 6, p. 317, 1976.","journal-title":"Acta Informatica"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0304-3975(76)90031-1","volume":"2","author":"J.W. Bakker De","year":"1976","unstructured":"DE BAKKER, J.W., Least fixed points revisited, Theoretical Computer Science, 2, pp. 155\u2013181, 1976.","journal-title":"Theoretical Computer Science"},{"unstructured":"DE BAKKER, J.W., Mathematical Theory of Program Correctness, Prentice-Hall International, 1980.","key":"7_CR4"},{"unstructured":"BARENDREGT, H.P., The Lambda Calculus, its Syntax and Semantics, North-Holland, 1981.","key":"7_CR5"},{"unstructured":"DE BRUIN, A., On the existence of Cook semantics, Report IW 163\/81, Mathematisch Centrum, 1981.","key":"7_CR6"},{"key":"7_CR7","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 language constructs for which it is impossible to obtain good Hoare-like axiom systems, J. ACM, 26, pp. 129\u2013147, 1979.","journal-title":"J. ACM"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/BF00288686","volume":"1","author":"M. Clint","year":"1972","unstructured":"CLINT, M. & C.A.R. HOARE, Program proving: jumps and functions, Acta Informatica, 1, pp. 214\u2013224, 1972.","journal-title":"Acta Informatica"},{"key":"7_CR9","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. on Comp., 7, pp. 70\u201390, 1978.","journal-title":"SIAM J. on Comp."},{"doi-asserted-by":"crossref","unstructured":"GORDON, M., R. MILNER & C. WADSWORTH, Edinburgh LCF, Lecture Notes in Computer Science 78, Springer, 1979.","key":"7_CR10","DOI":"10.1007\/3-540-09724-4"},{"unstructured":"GORELICK, G.A., A complete axiomatic system for proving assertions about recursive and non-recursive programs, Technical Report 75, Dept. of Comp. Science, University of Toronto, 1975.","key":"7_CR11"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1137\/0209005","volume":"9","author":"M.C.B. Hennessy","year":"1980","unstructured":"HENNESSY, M.C.B., The semantics of call-by-value and call-by-name in a nondeterministic environment, SIAM J. on Comp., 9, pp. 67\u201384, 1980.","journal-title":"SIAM J. on Comp."},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0304-3975(80)90015-8","volume":"11","author":"M.C.B. Hennessy","year":"1980","unstructured":"HENNESSY, M.C.B. & E.A. ASHCROFT, A mathematical semantics for a nondeterministic typed lambda calculus, Theoretical Comp. Science, 11, pp. 227\u2013246, 1980.","journal-title":"Theoretical Comp. Science"},{"key":"7_CR14","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"HOARE, C.A.R., An axiomatic basis for computer programming, CACM, 12, pp. 576\u2013580, 1969.","journal-title":"CACM"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/322003.322016","volume":"24","author":"N.D. Jones","year":"1977","unstructured":"JONES, N.D. & S.S. MUCHNIK, Even simple programs are hard to analyze, JACM, 24, pp. 338\u2013350, 1977.","journal-title":"JACM"},{"unstructured":"KLOP, J.W., Combinatory Reduction Systems, Mathematical Centre Tracts 127, Mathematisch Centrum, 1980.","key":"7_CR16"},{"doi-asserted-by":"crossref","unstructured":"LANGMAACK, H. & E.R. OLDEROG. Present-day Hoare-like systems for programming languages with procedures: power, limits, and most likely extensions, in Proc. 7th Coll. Automata, Languages and Programming (J.W. de Bakker & J. van Leeuwen, eds), Lecture Notes in Computer Scence 85, Springer, 1980.","key":"7_CR17","DOI":"10.1007\/3-540-10003-2_84"},{"doi-asserted-by":"crossref","unstructured":"LIPTON, R.J., A necessary and sufficient condition for the existence of Hoare logics, in Proc. IEEE Symposium Foundations of Computer Science, pp. 1\u20136, 1977.","key":"7_CR18","DOI":"10.1109\/SFCS.1977.1"},{"unstructured":"O'DONNELL, M., A critique on the foundations of Hoare-style programming logics, Technical Report, Purdue University, 1980.","key":"7_CR19"},{"key":"7_CR20","doi-asserted-by":"publisher","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, Theoretical Comp. Science, 5, pp. 223\u2013256, 1977.","journal-title":"Theoretical Comp. Science"},{"doi-asserted-by":"crossref","unstructured":"REYNOLDS, J.C., On the relation between direct and continuation semantics, in Proc. 2nd Coll. Automata, Languages and Programming (J. Loeckx, ed.), pp. 141\u2013156, Lecture Notes in Computer Science 14, Springer, 1974.","key":"7_CR21","DOI":"10.1007\/978-3-662-21545-6_10"},{"key":"7_CR22","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"TAIT, W.W., Intentional interpretation of functionals of finite type I, J. Symbolic Logic, 32, pp. 198\u2013212, 1967.","journal-title":"J. Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"TROELSTRA, A.S. et al., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lect. Notes in Mathematics 344, Springer, 1973.","key":"7_CR23","DOI":"10.1007\/BFb0066739"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0025776","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T23:29:33Z","timestamp":1578526173000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0025776"}},"subtitle":["extended abstract"],"short-title":[],"issued":{"date-parts":[[1982]]},"ISBN":["9783540112129","9783540390473"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0025776","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1982]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}