{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:45Z","timestamp":1725631965077},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105396","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"51-60","source":"Crossref","is-referenced-by-count":4,"title":["Inference rules for programming languages with side effects in expressions"],"prefix":"10.1007","author":[{"given":"Paul E.","family":"Black","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phillip J.","family":"Windley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1109\/HOL.1991.596288","volume-title":"Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications (HOL\u2019 91)","author":"S. Agerholm","year":"1991","unstructured":"Sten Agerholm, \u201cMechanizing Program Verification in HOL,\u201d in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications (HOL\u2019 91), edited by Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, IEEE Computer Society Press, Los Alamitos, California, 1991, pp. 208\u2013222."},{"issue":"2","key":"4_CR2","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BF00264021","volume":"11","author":"M. A. Arbib","year":"1972","unstructured":"Michael A. Arbib and Suad Alagi\u0107, \u201cProof Rules for Gotos,\u201d Acta Information, Vol. 11, No. 2, 1972, pp. 139\u2013148.","journal-title":"Acta Information"},{"key":"4_CR3","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-60275-5_56","volume-title":"Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95)","author":"P. E. Black","year":"1995","unstructured":"Paul E. Black and Phillip J. Windley, \u201cAutomatically Synthesized Term Denotation Predicates: A Proof Aid,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95), edited by E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, Springer-Verlag, Berlin, Germany, 1995, pp. 46\u201357."},{"key":"4_CR4","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/3-540-60275-5_60","volume-title":"Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95)","author":"H. Busch","year":"1995","unstructured":"Holger Busch, \u201cA Practical Method for Reasoning about Distributed Systems in a Theorem Prover,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95), edited by E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, Springer-Verlag, Germany, 1995, pp. 106\u2013121."},{"key":"4_CR5","unstructured":"Frederick B. Cohen, \u201cWhy is thttpd Secure?\u201d http:\/\/all.net\/ManAl\/white\/whitepaper.html or http:\/\/all.net\/ \u2192 Products \u2192 Secure http and gopher daemons (14 March 1996)."},{"key":"4_CR6","unstructured":"Frederick B. Cohen, \u201cA Secure World Wide Web Daemon,\u201d Computers and Security, submitted, 1995."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Paul Curzon, \u201cDeriving Correctness Properties of Compiled Code,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 92), edited by Luc Claesen and Michael Gordon, Elsevier Science Publishers, 1992, pp. 97\u2013116.","DOI":"10.1016\/B978-0-444-89880-7.50027-9"},{"key":"4_CR8","unstructured":"Nissim Francez, Program Verification. Addison-Wesley, 1992."},{"key":"4_CR9","volume-title":"Programming Language Theory and its Implementation","author":"J. C. G. Michael","year":"1988","unstructured":"Michael J. C. Gordon, Programming Language Theory and its Implementation. Prentice-Hall, Inc., New Jersey, 1988."},{"issue":"4","key":"4_CR10","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1145\/357114.357119","volume":"2","author":"G. David","year":"1980","unstructured":"David Gries & Gary Levin, \u201cAssignment and Procedure Call Proof Rules,\u201d ACM Transactions on Programming Languages and Systems, vol. 2, no. 4, Oct 1980, pp. 564\u2013579.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/HOL.1991.596271","volume-title":"Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications (HOL\u2019 91)","author":"R. Hale","year":"1991","unstructured":"Roger Hale, \u201cReasoning About Software,\u201d in Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications (HOL\u2019 91), edited by Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, IEEE Computer Society Press, Los Alamitos, California, 1991, pp. 52\u201358."},{"key":"4_CR12","unstructured":"Samuel P. Harbison and Guy L. Steele Jr., C, A Reference Manual. Prentice-Hall, Inc., 1991."},{"key":"4_CR13","unstructured":"William L. Harrison, Karl N. Levitt, Myla Archer, \u201cA HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 92), edited by Luc Claesen and Michael Gordon, Elsevier Science Publishers B.V., 1992, pp. 117\u2013126."},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"C. A. R. Hoare, \u201cAn Axiomatic Basis for Computer Programming,\u201d Communications of the ACM, vol. 12, October 1969, pp. 576\u2013583.","journal-title":"Communications of the ACM"},{"key":"4_CR15","volume-title":"Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures","author":"Peter Vincent Homeier","year":"1995","unstructured":"Peter Vincent Homeier, Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures, Ph.D. Dissertation, University of California, Los Angeles, 1995."},{"key":"4_CR16","unstructured":"HP-UX on-line manual, HP-UX Release 9.0: August 1992, Hewlett-Packard Company, Palo Alto, California."},{"key":"4_CR17","unstructured":"Derek Jones, \u201cChecking an Application's use of API,\u201d http:\/\/www.knosof.co.uk\/apichk.html (14 March 1996)."},{"key":"4_CR18","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/3-540-60275-5_67","volume-title":"Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95)","author":"S. Kalvala","year":"1995","unstructured":"Sara Kalvala, \u201cA Formulation of TLA in Isabelle,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95), edited by E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, Springer-Verlag, Berlin, Germany, 1995, pp. 214\u2013228."},{"key":"4_CR19","unstructured":"John P. Van Tassel, \u201cThe HOL parser Library,\u201d http:\/\/lal.cs.byu.edu\/lal\/holdoc\/library.html (13 June 1996)."},{"key":"4_CR20","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-60275-5_78","volume-title":"Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95)","author":"C. Zhang","year":"1995","unstructured":"Cui Zhang, Brian R. Becker, Mark R. Heckman, Karl Levitt, and Ron A. Olsson, \u201cA Hierarchical Method for Reasoning about Distributed Programming Languages,\u201d in Higher Order Logic Theorem Proving and Its Applications (HOL\u2019 95), edited by E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, Springer-Verlag, Berlin, Germany, 1995, pp. 385\u2013400."}],"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\/BFb0105396","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T22:52:28Z","timestamp":1639608748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105396"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0105396","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}