{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:21Z","timestamp":1725665001330},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_81","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:49:52Z","timestamp":1330292992000},"page":"201-215","source":"Crossref","is-referenced-by-count":8,"title":["Mechanical verification of mutually recursive procedures"],"prefix":"10.1007","author":[{"given":"Peter V.","family":"Homeier","sequence":"first","affiliation":[]},{"given":"David F.","family":"Martin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"18_CR1","unstructured":"Camilleri, J., Melham, T.: Reasoning with Inductively Defined Relations in the HOL Theorem Prover. Technical Report No. 265, University of Cambridge Computer Laboratory, August 1992"},{"issue":"No.1","key":"18_CR2","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S. Cook","year":"1978","unstructured":"Cook, S.: Soundness and Completeness of an Axiom System for Program Verification. SIAM Journal on Computing, Vol. 7, No. 1 (February 1978) 70\u201390","journal-title":"SIAM Journal on Computing"},{"key":"18_CR3","unstructured":"Cousineau, G., Gordon, M., Huet, G., Milner, R., Paulson, L., Wadsworth, C.: The ML Handbook. INRIA (1986)"},{"key":"18_CR4","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/978-1-4612-3658-0_10","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M. Gordon","year":"1989","unstructured":"Gordon, M.: Mechanizing Programming Logics in Higher Order Logic, in Current Trends in Hardware Verification and Automated Theorem Proving, ed. P.A. Subrahmanyam and G. Birtwistle.Springer-Verlag, New York (1989) 387\u2013439"},{"key":"18_CR5","volume-title":"Introduction to HOL, A Theorem Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL, A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1145\/357114.357119","volume":"2","author":"D. Gries","year":"1980","unstructured":"Gries, D., Levin, G.: Assignment and Procedure Call Proof Rules. ACM TOPLAS 2 (1980) 564\u2013579","journal-title":"ACM TOPLAS"},{"key":"18_CR7","first-page":"211","volume-title":"Formal Description of Programming Language Concepts","author":"J. Guttag","year":"1978","unstructured":"Guttag, J., Horning, J., London, R.: A Proof Rule for Euclid Procedures, in Formal Description of Programming Language Concepts, ed. E.J. Neuhold, North-Holland, Amsterdam (1978) 211\u2013220"},{"issue":"No.2","key":"18_CR8","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/comjnl\/38.2.131","volume":"38","author":"P. Homeier","year":"1995","unstructured":"Homeier, P., Martin, D.: A Mechanically Verified Verification Condition Generator. The Computer Journal 38 No. 2 (1995) 131\u2013141","journal-title":"The Computer Journal"},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S. Igarashi","year":"1975","unstructured":"Igarashi, S., London, R., Luckham, D.: Automatic Program Verification I: A Logical Basis and its Implementation. ACTA Informatica 4 (1975) 145\u2013182","journal-title":"ACTA Informatica"},{"key":"18_CR10","first-page":"350","volume-title":"A Package for Inductive Relation Definitions in HOL","author":"T. Melham","year":"1992","unstructured":"Melham, T.: A Package for Inductive Relation Definitions in HOL, in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, ed. Archer, M., Joyce, J., Levitt, K., Windley, P. IEEE Computer Society Press (1992) 350\u2013357"},{"key":"18_CR11","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-10843-2_30","volume":"115","author":"M. Moriconi","year":"1981","unstructured":"Moriconi, M., Schwartz, R.: Automatic Construction of Verification Condition Generators From Hoare Logics, in Proceedings of ICALP 8, Springer Lecture Notes in Computer Science 115 (1981) 363\u2013377","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"18_CR12","unstructured":"Ragland, L.: A Verified Program Verifier. Technical Report No. 18, Department of Computer Sciences, University of Texas at Austin (May 1973)"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0167-6423(84)90017-0","volume":"4","author":"S. Sokolowski","year":"1984","unstructured":"Sokolowski, S.: Partial Correctness: The Term-Wise Approach. Science of Computer Programming 4 (1984) 141\u2013157","journal-title":"Science of Computer Programming"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90149-1","volume":"59","author":"A. Stoughton","year":"1988","unstructured":"Stoughton, A.: Substitution Revisited. Theoretical Computer Science 59 (1988) 317\u2013325","journal-title":"Theoretical Computer Science"},{"key":"18_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages, An Introduction","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages, An Introduction. The MIT Press, Cambridge, Massachusetts (1993)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_81.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:33:41Z","timestamp":1619573621000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_81"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_81","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}