{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:26:43Z","timestamp":1748071603073,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"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":[[2002]]},"DOI":"10.1007\/3-540-45685-6_22","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"332-347","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Weakest Precondition for General Recursive Programs Formalized in Coq"],"prefix":"10.1007","author":[{"given":"Xingyuan","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malcolm","family":"Munro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Harman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lin","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"issue":"6","key":"22_CR1","doi-asserted-by":"crossref","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R. J. R. Back","year":"1988","unstructured":"R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593\u2013624, August 1988.","journal-title":"Acta Informatica"},{"key":"22_CR2","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu noz, C. Murthy, C. Parent, C. Paulin, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant Reference Manual-Version V6.1. Technical Report 0203, INRIA, August 1997."},{"key":"22_CR3","volume-title":"Technical report 94-44","author":"D. Carrington","year":"1994","unstructured":"D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. Refinement in Ergo. Technical report 94-44, Software Verification Research Centre, School of Information Technology, The University of Queensland, Brisbane 4072. Australia, November 1994."},{"key":"22_CR4","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76:96\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"22_CR5","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"22_CR6","series-title":"Lect Notes Comput Sci","volume-title":"International Workshop, TYPES\u2019 98, Kloster Irsee, Germany","author":"J.-C. Filli\u00e2tre","year":"1998","unstructured":"J.-C. Filli\u00e2tre. Proof of Imperative Programs in Type Theory. In International Workshop, TYPES\u2019 98, Kloster Irsee, Germany, volume 1657 of Lecture Notes in Computer Science. Springer-Verlag, March 1998."},{"key":"22_CR7","unstructured":"T. Kleymann. Hoare Logic and VDM: M achine-Checked Soundness and Completeness Proofs. Ph.D. thesis, University of Edinburgh, 1998."},{"key":"22_CR8","unstructured":"J. Knappmann. A PVS based tool for developing programs in the refinement calculus. Marster\u2019s Thesis, Christian-Albrechts-University, 1996."},{"key":"22_CR9","volume-title":"Technical Report TUCS-TR-252","author":"L. Laibinis","year":"1999","unstructured":"L. Laibinis and J. von Wright. Functional procedures in higher-order logic. Technical Report TUCS-TR-252, Turku Centre for Computer Science, Finland, March 15, 1999."},{"key":"22_CR10","series-title":"Master\u2019s Thesis","volume-title":"A formalization of Dijkstra\u2019s predicate transformer wp in Martin-Lof type theory","author":"L. Lindqvist","year":"1997","unstructured":"L. Lindqvist. A formalization of Dijkstra\u2019s predicate transformer wp in Martin-Lof type theory. Master\u2019s Thesis, Linkopin University, Sweden, 1997."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"issue":"3","key":"22_CR12","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/44501.44503","volume":"10","author":"C. Morgan","year":"1988","unstructured":"C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3):403\u2013419, July 1988.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"22_CR13","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. M. Morris","year":"1987","unstructured":"J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287\u2013306, December 1987.","journal-title":"Science of Computer Programming"},{"key":"22_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-62034-6_48","volume-title":"Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science","author":"T. Nipkow","year":"1996","unstructured":"T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science, pages 180\u2013192. Springer-Verlag LNCS 1180, 1996."},{"key":"22_CR15","series-title":"International Series of Monographs on Computer Science","volume-title":"Programming in Martin-Lof\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Peterson, and J. M. Smith. Programming in Martin-Lof\u2019s Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, New York, NY, 1990."},{"key":"22_CR16","volume-title":"Reports on Computer Science & Mathematics Series A\u201485","author":"R. J. R. Back","year":"1989","unstructured":"R. J. R. Back and J. von Wright. Refinement concepts formalized in higher-order logic. Reports on Computer Science & Mathematics Series A\u201485, Institutionen f\u00f6r Informationsbehandling & Mathematiska Institutet, \u00c5bo Akademi, Lemmink:ainengatan 14, SF-20520 Turku, Finland, September 1989."},{"key":"22_CR17","unstructured":"M. Staples. A Mechanised Theory of Refinement. Ph.D. Dissertation, Computer Laboratory, University of Cambridge, 1998."},{"key":"22_CR18","series-title":"Lect Notes Comput Sci","volume-title":"TPHOLs: The 12th International Conference on Theorem Proving in Higher-Order Logics","author":"M. Staples","year":"1999","unstructured":"M. Staples. Program transformations and refinements in HOL. In Y. Bertot G. Dowek, C. Paulin, editor, TPHOLs: The 12th International Conference on Theorem Proving in Higher-Order Logics. LNCS, Springer-Verlag., 1999."},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"J. von Wright and K. Sere. Program transformations and refinements in HOL. In Myla Archer, Jennifer J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, Proceedigns of the International Workshop on the HOL Theorem Proving System and its Applications, pages 231\u2013241, Los Alamitos, CA, USA, August 1992. IEEE Computer Society Press.","DOI":"10.1109\/HOL.1991.596290"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T13:30:53Z","timestamp":1737034253000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"25 July 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}