{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:50Z","timestamp":1725467510852},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055136","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"171-188","source":"Crossref","is-referenced-by-count":3,"title":["Formalizing Dijkstra"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"11_CR1","volume-title":"Volume 131 of Mathematical Centre Tracts","author":"R. Back","year":"1980","unstructured":"R. Back. Correctness Preserving Program Transformations: Proof Theory and Applications, Volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam, 1980."},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R. DeMillo","year":"1979","unstructured":"R. DeMillo, R. Lipton, and A. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22, 271\u2013280, 1979.","journal-title":"Communications of the ACM"},{"doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra. Trip report visit ETH Zurich, EWD474, 3\u20134 February 1975. See [8], pp. 95\u201398.","key":"11_CR3","DOI":"10.1007\/978-1-4612-5695-3_17"},{"unstructured":"E. E. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.","key":"11_CR4"},{"doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra. Formal techniques and sizeable programs, EWD563. See [8], pp. 205\u2013214, 1976. Paper prepared for Symposium on the Mathematical Foundations of Computing Science, Gdansk 1976.","key":"11_CR5","DOI":"10.1007\/3-540-07804-5_31"},{"doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra. A somewhat open letter to EAA or: Why I proved the boundedness of the nondeterminacy in the way I did, EWD614, 1977. See [8], pp. 284\u2013287.","key":"11_CR6","DOI":"10.1007\/978-1-4612-5695-3_51"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1005888.1005890","volume":"3","author":"E. W. Dijkstra","year":"1978","unstructured":"E. W. Dijkstra. On a political pamphlet from the middle ages. ACM SIGSOFT, Software Engineering Notes, 3, 14, 1978.","journal-title":"ACM SIGSOFT, Software Engineering Notes"},{"doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra (ed.). Selected Writings on Computing: A Personal Perspective. Springer-Verlag, 1982.","key":"11_CR8","DOI":"10.1007\/978-1-4612-5695-3"},{"doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwistle and P. A. Subrahmanyam (eds.), Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439. Springer-Verlag, 1989.","key":"11_CR9","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"11_CR10","first-page":"8","volume-title":"Volume 735 of Lecture Notes in Computer Science","author":"J. Grundy","year":"1993","unstructured":"J. Grundy. Predicative programming \u2014 a survey. In D. Bj\u00d8rner, M. Broy, and I. V. Pottosin (eds.), Formal Methods in Programming and Their Applications: Proceedings of the International Conference, Volume 735 of Lecture Notes in Computer Science, Academgorodok, Novosibirsk, Russia, pp. 8\u201325. Springer-Verlag, 1993."},{"doi-asserted-by":"crossref","unstructured":"W. H. Hesselink. Programs, Recursion and Unbounded Choice, Volume 27 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.","key":"11_CR11","DOI":"10.1017\/CBO9780511569784"},{"volume-title":"Volume 780 of Lecture Notes in Computer Science","year":"1993","unstructured":"J. J. Joyce and C. Seger (eds.). Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, Volume 780 of Lecture Notes in Computer Science, UBC, Vancouver, Canada. Springer-Verlag, 1993.","key":"11_CR12"},{"key":"11_CR13","first-page":"43","volume-title":"Volume 780 of Lecture Notes in Computer Science","author":"D. Syme","year":"1993","unstructured":"D. Syme. Reasoning with the formal definition of Standard ML in HOL. See [12], pp. 43\u201360."},{"key":"11_CR14","first-page":"61","volume-title":"Volume 780 of Lecture Notes in Computer Science","author":"M. VanInwegen","year":"1993","unstructured":"M. VanInwegen and E. Gunter. HOL-ML. See [12], pp. 61\u201374."},{"key":"11_CR15","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BF01383984","volume":"3","author":"J. Wright von","year":"1993","unstructured":"J. von Wright, J. Hekanaho, P. Luostarinen, and T. L\u00e5ngbacka. Mechanizing some advanced refinement concepts. Formal Methods in System Design, 3, 49\u201382, 1993.","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055136","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T11:49:46Z","timestamp":1627645786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0055136","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}