{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:23:41Z","timestamp":1743027821904,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540092513"},{"type":"electronic","value":"9783540353126"}],"license":[{"start":{"date-parts":[[1979,1,1]],"date-time":"1979-01-01T00:00:00Z","timestamp":283996800000},"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":[[1979]]},"DOI":"10.1007\/bfb0014666","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T05:25:49Z","timestamp":1132723549000},"page":"133-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof rules for the programming language Euclid"],"prefix":"10.1007","author":[{"given":"R. L.","family":"London","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. V.","family":"Guttag","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. J.","family":"Horning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B. W.","family":"Lampson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. G.","family":"Mitchell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G. J.","family":"Popek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"17_CR1","first-page":"10","volume-title":"Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems","author":"E. M. Clarke Jr.","year":"1977","unstructured":"Clarke, E. M. Jr.: Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems. Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 10\u201320. New York: ACM 1977"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Complementary Definitions of Programming Language Semantics","author":"J. E. Donahue","year":"1976","unstructured":"Donahue, J. E.: Complementary Definitions of Programming Language Semantics. Lecture Notes in Computer Science, Vol. 42. Berlin-Heidelberg-New York: Springer 1976"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/BF00289246","volume":"8","author":"G. W. Ernst","year":"1977","unstructured":"Ernst, G. W.: Rules of inference for procedure calls. Acta Informatica 8, 145\u2013152 (1977)","journal-title":"Acta Informatica"},{"key":"17_CR4","unstructured":"Guttag, J. V., Horning, J. J., and London, R. L.: A proof rule for Euclid procedures. Working Conference on Formal Description of Programming Concepts, Preprints of Technical Papers, (E. Neuhold, ed.), St. Andrews, New Brunswick, pp. 10.1\u201310.8. Publication by North Holland forthcoming. Also USC Information Sciences Institute, Technical Report ISI\/RR-77-60, May 1977"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Guttag, J. V., Horowitz, E., and Musser, D. R.: Abstract data types and software validation. USC Information Sciences Institute, Technical Report ISI\/RR-76-48, August 1976","DOI":"10.21236\/ADA029896"},{"key":"17_CR6","doi-asserted-by":"publisher","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. Comm. ACM 12, 576\u2013580 and 583 (1969)","journal-title":"Comm. ACM"},{"key":"17_CR7","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symposium on Semantics of Algorithmic Languages","author":"C. A. R. Hoare","year":"1971","unstructured":"Hoare, C. A. R.: Procedures and parameters: An axiomatic approach. In: Symposium on Semantics of Algorithmic Languages (E. Engeler, ed.), Lecture Notes in Mathematics, Vol. 188, pp. 102\u2013116. Berlin-Heidelberg-New York: Springer 1971"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C. A. R. Hoare","year":"1972","unstructured":"Hoare, C. A. R.: Proof of correctness of data representations. Acta Informatica 1, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C. A. R. Hoare","year":"1973","unstructured":"Hoare, C. A. R. and Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica 2, 335\u2013355 (1973)","journal-title":"Acta Informatica"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-9984-5","volume-title":"PASCAL User Manual and Report","author":"K. Jensen","year":"1975","unstructured":"Jensen, K. and Wirth, N.: PASCAL User Manual and Report. Lecture Notes in Computer Science, Vol. 18, 2nd ed. Berlin-Heidelberg-New York: Springer 1975","edition":"2nd ed."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Lampson, B. W., Horning, J. J., London, R. L., Mitchell, J. G., and Popek, G. J.: Revised report on the programming language Euclid (to appear). An earlier version appeared in SIGPLAN Notices, 12, No. 2, February 1977","DOI":"10.1145\/954666.971189"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Musser, D. R.: A proof rule for functions. USC Information Sciences Institute, Technical Report ISI\/RR-77-62, October 1977","DOI":"10.21236\/ADA046298"},{"issue":"3","key":"17_CR13","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/390017.808307","volume":"12","author":"G. J. Popek","year":"1977","unstructured":"Popek, G. J., Horning, J. J., Lampson, B. W., Mitchell, J. G., and London, R. L.: Notes on the design of Euclid. Proceedings of an ACM Conference on Language Design for Reliable Software, Raleigh, North Carolina, SIGPLAN Notices, 12, No. 3, 11\u201318 (1977)","journal-title":"SIGPLAN Notices"},{"key":"17_CR14","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF00288745","volume":"4","author":"J. Spitzen","year":"1975","unstructured":"Spitzen, J. and Wegbreit, B.: The verification and synthesis of data structures. Acta Informatica 4, 127\u2013144 (1975)","journal-title":"Acta Informatica"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/BF00264291","volume":"1","author":"N. Wirth","year":"1971","unstructured":"Wirth, N.: The programming language PASCAL. Acta Informatica 1, 35\u201363 (1971)","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","Program Construction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014666","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,19]],"date-time":"2022-08-19T05:03:25Z","timestamp":1660885405000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0014666"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979]]},"ISBN":["9783540092513","9783540353126"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0014666","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1979]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}